src/FOLP/ex/intro.ML
changeset 15531 08c8dad8e399
parent 3836 f1a1817659e6
child 15661 9ef583b08647
--- a/src/FOLP/ex/intro.ML	Fri Feb 11 18:51:00 2005 +0100
+++ b/src/FOLP/ex/intro.ML	Sun Feb 13 17:15:14 2005 +0100
@@ -12,7 +12,7 @@
 *)
 
 
-(**** Some simple backward proofs ****)
+(**** SOME simple backward proofs ****)
 
 goal FOLP.thy "?p:P|P --> P";
 by (rtac impI 1);