src/FOLP/ex/intro.ML
changeset 15661 9ef583b08647
parent 15531 08c8dad8e399
child 17480 fd19f77dcf60
--- a/src/FOLP/ex/intro.ML	Thu Apr 07 09:24:35 2005 +0200
+++ b/src/FOLP/ex/intro.ML	Thu Apr 07 09:25:33 2005 +0200
@@ -12,7 +12,7 @@
 *)
 
 
-(**** SOME simple backward proofs ****)
+(**** Some simple backward proofs ****)
 
 goal FOLP.thy "?p:P|P --> P";
 by (rtac impI 1);