| changeset 12920 | 32292d83367b |
| parent 12437 | 6d4e02b6dd43 |
| child 13469 | 70d8dfef587d |
--- 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")