More description fixes

* Remove package name
* Start with upper case letter
* Remove trailing period

Also reword some descriptions and move some long descriptions to
longDescription.

I'm not touching generated packages.

4 files changed, 11 insertions, 15 deletions

diff --git a/pkgs/applications/science/logic/hol/default.nix b/pkgs/applications/science/logic/hol/default.nix
index 18a16114c50..4223c52b7d4 100644
--- a/pkgs/applications/science/logic/hol/default.nix
+++ b/pkgs/applications/science/logic/hol/default.nix
@@ -39,9 +39,8 @@ stdenv.mkDerivation {
   '';
 
   meta = {
-    description = "HOL4, an interactive theorem prover based on Higher-Order Logic.";
+    description = "Interactive theorem prover based on Higher-Order Logic";
     longDescription = ''
-
       HOL4 is the latest version of the HOL interactive proof
       assistant for higher order logic: a programming environment in
       which theorems can be proved and proof tools
@@ -52,7 +51,6 @@ stdenv.mkDerivation {
       engines. HOL4 is particularly suitable as a platform for
       implementing combinations of deduction, execution and property
       checking.
-
     '';
     homepage = "http://hol.sourceforge.net/";
     license = "BSD";
diff --git a/pkgs/applications/science/logic/hol_light/default.nix b/pkgs/applications/science/logic/hol_light/default.nix
index f9549241a45..d6c1c0c1878 100644
--- a/pkgs/applications/science/logic/hol_light/default.nix
+++ b/pkgs/applications/science/logic/hol_light/default.nix
@@ -26,15 +26,15 @@ stdenv.mkDerivation {
   '';
 
   meta = {
-    description = "An interactive theorem prover based on Higher-Order Logic.";
+    description = "Interactive theorem prover based on Higher-Order Logic";
     longDescription = ''
-HOL Light is a computer program to help users prove interesting mathematical
-theorems completely formally in Higher-Order Logic.  It sets a very exacting
-standard of correctness, but provides a number of automated tools and
-pre-proved mathematical theorems (e.g., about arithmetic, basic set theory and
-real analysis) to save the user work.  It is also fully programmable, so users
-can extend it with new theorems and inference rules without compromising its
-soundness.
+      HOL Light is a computer program to help users prove interesting
+      mathematical theorems completely formally in Higher-Order Logic.  It sets
+      a very exacting standard of correctness, but provides a number of
+      automated tools and pre-proved mathematical theorems (e.g., about
+      arithmetic, basic set theory and real analysis) to save the user work.
+      It is also fully programmable, so users can extend it with new theorems
+      and inference rules without compromising its soundness.
     '';
     homepage = http://www.cl.cam.ac.uk/~jrh13/hol-light/;
     license = stdenv.lib.licenses.bsd2;
diff --git a/pkgs/applications/science/logic/logisim/default.nix b/pkgs/applications/science/logic/logisim/default.nix
index 009bed3ffe2..ab46efa9a96 100644
--- a/pkgs/applications/science/logic/logisim/default.nix
+++ b/pkgs/applications/science/logic/logisim/default.nix
@@ -26,7 +26,7 @@ stdenv.mkDerivation {
   
   meta = {
     homepage = "http://ozark.hendrix.edu/~burch/logisim";
-    description = "Logisim is an educational tool for designing and simulating digital logic circuits.";
+    description = "Educational tool for designing and simulating digital logic circuits";
     license = "GPLv2+";
   };
 }
diff --git a/pkgs/applications/science/logic/prover9/default.nix b/pkgs/applications/science/logic/prover9/default.nix
index 93b1657aa14..d92c7887210 100644
--- a/pkgs/applications/science/logic/prover9/default.nix
+++ b/pkgs/applications/science/logic/prover9/default.nix
@@ -31,14 +31,12 @@ stdenv.mkDerivation {
   meta = {
     homepage = "http://www.cs.unm.edu/~mccune/mace4/";
     license = "GPL";
-    description = "Prover9 is an automated theorem prover for first-order and equational logic.";
-
+    description = "Automated theorem prover for first-order and equational logic";
     longDescription = ''
       Prover9 is a resolution/paramodulation automated theorem prover
       for first-order and equational logic. Prover9 is a successor of
       the Otter Prover. This is the LADR command-line version.
     '';
-
     platforms = stdenv.lib.platforms.unix;
     maintainers = [];
   };