doc-src/TutorialI/Inductive/AB.thy

--- a/doc-src/TutorialI/Inductive/AB.thy	Mon Oct 16 10:59:35 2000 +0200
+++ b/doc-src/TutorialI/Inductive/AB.thy	Mon Oct 16 13:21:01 2000 +0200
@@ -1,4 +1,6 @@
-theory AB = Main:;
+(*<*)theory AB = Main:(*>*)
+
+section{*A context free grammar*}
 
 datatype alfa = a | b;
 
@@ -118,4 +120,4 @@
  apply(force simp add:min_less_iff_disj);
 by(force simp add:min_less_iff_disj split add: nat_diff_split);
 
-end;
+(*<*)end(*>*)