doc-src/TutorialI/Datatype/ABexpr.thy
changeset 16417 9bc16273c2d4
parent 12334 60bf75e157e4
child 27015 f8537d69f514
     1.1 --- a/doc-src/TutorialI/Datatype/ABexpr.thy	Fri Jun 17 11:35:35 2005 +0200
     1.2 +++ b/doc-src/TutorialI/Datatype/ABexpr.thy	Fri Jun 17 16:12:49 2005 +0200
     1.3 @@ -1,5 +1,5 @@
     1.4  (*<*)
     1.5 -theory ABexpr = Main:;
     1.6 +theory ABexpr imports Main begin;
     1.7  (*>*)
     1.8  
     1.9  text{*