--- a/src/HOL/Isar_examples/BasicLogic.thy Fri May 28 11:42:07 1999 +0200
+++ b/src/HOL/Isar_examples/BasicLogic.thy Fri May 28 13:30:59 1999 +0200
@@ -77,7 +77,7 @@
qed;
-(* propositional proof (from 'Introduction to Isabelle') *)
+text {* propositional proof (from 'Introduction to Isabelle') *};
lemma "P | P --> P";
proof;
@@ -97,7 +97,7 @@
qed;
-(* quantifier proof (from 'Introduction to Isabelle') *)
+text {* quantifier proof (from 'Introduction to Isabelle') *};
lemma "(EX x. P(f(x))) --> (EX x. P(x))";
proof;