diff --git a/index.all b/index.all
index a21c557..7d3ca43 100644
--- a/index.all
+++ b/index.all
@@ -14,11 +14,11 @@ $Path = Join[$Path, {"/afs/user/xzhao/analytica/analytica", "/afs/user/xzhao/ana
 
 (* Quantification. *)
 
-<<quantify.M;
+<<quantify.m;
 
 (* Simplify the sequent to be proved. *)
 
-<<simplify.M;
+<<simplify.m;
 
 (* Rewrite the sequent to be proved. *)
 
diff --git a/system_interface.M b/system_interface.M
index 4a8b3a4..a96673e 100644
--- a/system_interface.M
+++ b/system_interface.M
@@ -5,14 +5,14 @@
 BeginPackage["SystemInterface`"]
 
 
-(* these functions are provided in package simplify.M *)
+(* these functions are provided in package simplify.m *)
 
 NIL::usage =
 	" NIL denotes True in a conjunction, False in a disjunction. ";
 
 SimplifyMessage::usage =
 	" SimplifyMessage is a list of rules and formulas which are \
-	results of intermediate steps of simplification. "
+	results of intermediate steps of simplification. ";
 
 SimplifyIfChanged::usage =
 	" SimplifyIfChanged[f1, f2] gives StrongSimplify[f2] as answer \
@@ -86,7 +86,7 @@ UserFunctions::usage =
 
 GivenFormulas::usage =
 	" GivenFormulas is a list of given properties which can be seen \
-	using PrintGiven. "
+	using PrintGiven. ";
 
 
 (* these functions are provided in package inequality.M *)
@@ -108,7 +108,7 @@ RulesForRelations::usage =
 	of some equations and inequalities. ";
 
 DepthCount::usage = 
-	" DepthCount is the current depth for using bound to prove 
+	" DepthCount is the current depth for using bound to prove \
 	inequalities. ";
 
 
@@ -140,7 +140,7 @@ Factorize::usage =
 	where R is either ==, <= or <. ";
 
 
-(* these functions are provided in package quantify.M *)
+(* these functions are provided in package quantify.m *)
 
 
 substitution::usage = 
@@ -168,7 +168,7 @@ Requantify::usage =
 	PositivePosition. ";
 
 PositivePosition::usage =
-	" PositivePosition means the positive position in a sequent. 
+	" PositivePosition means the positive position in a sequent. \
 	(See also quantify) ";
 
 NegativePosition::usage =
@@ -208,8 +208,8 @@ MaxMinRules::usage =
 	" MaxMinRules is a set of local rules about maximum or minimum \
 	values, it is used in simplification. ";
 
-GosperSum::usage = "GosperSum[term, {var, n0, n1}] attempts to find the value 
-	of Sum[term, {var, n0, n1}] for symbolic n0, n1."
+GosperSum::usage = "GosperSum[term, {var, n0, n1}] attempts to find \
+    the value of Sum[term, {var, n0, n1}] for symbolic n0, n1.";
 
 SimplifySummation::usage =
 	" SimplifySummation[i][f] tries ith method to simplify the summation \
diff --git a/user_interface.M b/user_interface.M
index 2c0463f..41abe12 100644
--- a/user_interface.M
+++ b/user_interface.M
@@ -4,7 +4,7 @@
 
 BeginPackage["UserInterface`"]
 
-(* these functions are provided in package simplify.M *)
+(* these functions are provided in package simplify.m *)
 
 seq::usage = 
 	" seq[a, b] is the notation for a sequent, with hypothesis 'a' \
@@ -157,7 +157,7 @@ UserRules::usage =
 
 CurrentPath::usage = 
 	" CurrentPath is a list of the sections that contain the current \
-	context section as a subsection. "
+	context section as a subsection. ";
 
 
 CurrentSection::usage = 
@@ -208,7 +208,7 @@ SuccessStepsOnly::usage =
 	steps are printed out. ";
 
 EndDocument::usage =
-	" EndDocument is used to put the ending to the TeX file. "
+	" EndDocument is used to put the ending to the TeX file. ";
 
 Abbreviate::usage = 
 	"Abbreviate[f1, f2] takes 'f2' as an abbreviation for 'f1'. ";
@@ -285,7 +285,7 @@ Lower::usage =
 	" Lower[f] gives a set of lower bounds for 'f'. ";
 
 
-(* these functions are provided in the package quantify.M *)
+(* these functions are provided in the package quantify.m *)
 
 all::usage = 
 	" all[x, f] is the universal quantifier, ('f' holds for all 'x'). \
@@ -309,4 +309,4 @@ congruent::usage =
 	with respect 'c'. ";
 
 over;
-EndPackage[]
\ No newline at end of file
+EndPackage[]