include theory Record (tuned dependencies);
authorwenzelm
Thu, 21 Feb 2002 20:09:48 +0100
changeset 12920 32292d83367b
parent 12919 d6a0d168291e
child 12921 b7b0daf0d882
include theory Record (tuned dependencies);
src/HOL/Inductive.thy
--- a/src/HOL/Inductive.thy	Thu Feb 21 20:09:19 2002 +0100
+++ b/src/HOL/Inductive.thy	Thu Feb 21 20:09:48 2002 +0100
@@ -6,7 +6,7 @@
 
 header {* Support for inductive sets and types *}
 
-theory Inductive = Gfp + Sum_Type + Relation
+theory Inductive = Gfp + Sum_Type + Relation + Record
 files
   ("Tools/inductive_package.ML")
   ("Tools/inductive_codegen.ML")