author | wenzelm |
Thu, 21 Feb 2002 20:09:48 +0100 | |
changeset 12920 | 32292d83367b |
parent 12919 | d6a0d168291e |
child 12921 | b7b0daf0d882 |
--- 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")