diff -r 74e8f703f5f2 -r cf6ad8d22793 src/HOL/Isar_examples/BasicLogic.thy
--- 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;