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