src/LCF/ex/ROOT.ML
changeset 15531 08c8dad8e399
parent 9000 c20d58286a51
child 15661 9ef583b08647
     1.1 --- a/src/LCF/ex/ROOT.ML	Fri Feb 11 18:51:00 2005 +0100
     1.2 +++ b/src/LCF/ex/ROOT.ML	Sun Feb 13 17:15:14 2005 +0100
     1.3 @@ -3,7 +3,7 @@
     1.4      Author:     Tobias Nipkow
     1.5      Copyright   1991  University of Cambridge
     1.6  
     1.7 -Some examples from Lawrence Paulson's book Logic and Computation.
     1.8 +SOME examples from Lawrence Paulson's book Logic and Computation.
     1.9  *)
    1.10  
    1.11  time_use_thy "Ex1";