# HG changeset patch
# User wenzelm
# Date 1293621758 -3600
# Node ID 08a072ca634852a5eef558b773547fc24b75d23d
# Parent  2878845bc549ceef616d6856e0cb4448663a6884
tuned comments;

diff -r 2878845bc549 -r 08a072ca6348 src/HOL/Mutabelle/mutabelle.ML
--- a/src/HOL/Mutabelle/mutabelle.ML	Wed Dec 29 12:16:49 2010 +0100
+++ b/src/HOL/Mutabelle/mutabelle.ML	Wed Dec 29 12:22:38 2010 +0100
@@ -1,8 +1,9 @@
 (*  Title:      HOL/Mutabelle/mutabelle.ML
     Author:     Veronika Ortner, TU Muenchen
 
-    Mutation of theorems
+Mutation of theorems.
 *)
+
 signature MUTABELLE =
 sig
  val testgen_name : string Unsynchronized.ref
@@ -80,13 +81,10 @@
  end;
 
 
-(*helper function in order to properly print a term*)
+(*possibility to print a given term for debugging purposes*)
 
 fun prt x = Pretty.writeln (Syntax.pretty_term_global @{theory Main} x);
 
-
-(*possibility to print a given term for debugging purposes*)
-
 val debug = (Unsynchronized.ref false);
 fun debug_msg mutterm = if (!debug) then (prt mutterm) else ();
 
diff -r 2878845bc549 -r 08a072ca6348 src/HOL/Mutabelle/mutabelle_extra.ML
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Wed Dec 29 12:16:49 2010 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Wed Dec 29 12:22:38 2010 +0100
@@ -1,8 +1,9 @@
 (*  Title:      HOL/Mutabelle/mutabelle_extra.ML
     Author:     Stefan Berghofer, Jasmin Blanchette, Lukas Bulwahn, TU Muenchen
 
-    Invokation of Counterexample generators
+Invokation of Counterexample generators.
 *)
+
 signature MUTABELLE_EXTRA =
 sig