load / setup datatype package;
authorwenzelm
Mon Oct 04 21:43:45 1999 +0200 (1999-10-04)
changeset 770038b6d2643630
parent 7699 09d8fd81cc1f
child 7701 2c8c3b7003e5
load / setup datatype package;
src/HOL/Inductive.thy
     1.1 --- a/src/HOL/Inductive.thy	Mon Oct 04 21:43:05 1999 +0200
     1.2 +++ b/src/HOL/Inductive.thy	Mon Oct 04 21:43:45 1999 +0200
     1.3 @@ -1,7 +1,19 @@
     1.4 +(*  Title:      HOL/Inductive.thy
     1.5 +    ID:         $Id$
     1.6 +*)
     1.7  
     1.8  theory Inductive = Gfp + Prod + Sum
     1.9 -files "Tools/inductive_package.ML":
    1.10 +files
    1.11 +  "Tools/inductive_package.ML"
    1.12 +  "Tools/datatype_aux.ML"
    1.13 +  "Tools/datatype_prop.ML"
    1.14 +  "Tools/datatype_rep_proofs.ML"
    1.15 +  "Tools/datatype_abs_proofs.ML"
    1.16 +  "Tools/datatype_package.ML"
    1.17 +  "Tools/primrec_package.ML":
    1.18  
    1.19  setup InductivePackage.setup
    1.20 +setup DatatypePackage.setup
    1.21 +
    1.22  
    1.23  end