tuned comments;
authorwenzelm
Wed Dec 29 12:22:38 2010 +0100 (2010-12-29)
changeset 4140808a072ca6348
parent 41407 2878845bc549
child 41409 0bc364f772ef
tuned comments;
src/HOL/Mutabelle/mutabelle.ML
src/HOL/Mutabelle/mutabelle_extra.ML
     1.1 --- a/src/HOL/Mutabelle/mutabelle.ML	Wed Dec 29 12:16:49 2010 +0100
     1.2 +++ b/src/HOL/Mutabelle/mutabelle.ML	Wed Dec 29 12:22:38 2010 +0100
     1.3 @@ -1,8 +1,9 @@
     1.4  (*  Title:      HOL/Mutabelle/mutabelle.ML
     1.5      Author:     Veronika Ortner, TU Muenchen
     1.6  
     1.7 -    Mutation of theorems
     1.8 +Mutation of theorems.
     1.9  *)
    1.10 +
    1.11  signature MUTABELLE =
    1.12  sig
    1.13   val testgen_name : string Unsynchronized.ref
    1.14 @@ -80,13 +81,10 @@
    1.15   end;
    1.16  
    1.17  
    1.18 -(*helper function in order to properly print a term*)
    1.19 +(*possibility to print a given term for debugging purposes*)
    1.20  
    1.21  fun prt x = Pretty.writeln (Syntax.pretty_term_global @{theory Main} x);
    1.22  
    1.23 -
    1.24 -(*possibility to print a given term for debugging purposes*)
    1.25 -
    1.26  val debug = (Unsynchronized.ref false);
    1.27  fun debug_msg mutterm = if (!debug) then (prt mutterm) else ();
    1.28  
     2.1 --- a/src/HOL/Mutabelle/mutabelle_extra.ML	Wed Dec 29 12:16:49 2010 +0100
     2.2 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Wed Dec 29 12:22:38 2010 +0100
     2.3 @@ -1,8 +1,9 @@
     2.4  (*  Title:      HOL/Mutabelle/mutabelle_extra.ML
     2.5      Author:     Stefan Berghofer, Jasmin Blanchette, Lukas Bulwahn, TU Muenchen
     2.6  
     2.7 -    Invokation of Counterexample generators
     2.8 +Invokation of Counterexample generators.
     2.9  *)
    2.10 +
    2.11  signature MUTABELLE_EXTRA =
    2.12  sig
    2.13