src/HOL/Induct/Sexp.thy
changeset 16417 9bc16273c2d4
parent 13079 e7738aa7267f
child 18413 50c0c118e96d
--- a/src/HOL/Induct/Sexp.thy	Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Induct/Sexp.thy	Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
 structures by hand.
 *)
 
-theory Sexp = Datatype_Universe + Inductive:
+theory Sexp imports Datatype_Universe Inductive begin
 consts
   sexp      :: "'a item set"