tuned Inductive.thy;
authorwenzelm
Wed Jul 01 11:33:39 1998 +0200 (1998-07-01)
changeset 51050ff5bec04d02
parent 5104 230cca8452c7
child 5106 05b7c9a2ddf9
tuned Inductive.thy;
src/HOL/Inductive.thy
src/HOL/ROOT.ML
     1.1 --- a/src/HOL/Inductive.thy	Wed Jul 01 11:20:32 1998 +0200
     1.2 +++ b/src/HOL/Inductive.thy	Wed Jul 01 11:33:39 1998 +0200
     1.3 @@ -1,4 +1,2 @@
     1.4 -Inductive = Gfp + Prod + Sum +
     1.5  
     1.6 -end
     1.7 -
     1.8 +Inductive = Gfp + Prod + Sum
     2.1 --- a/src/HOL/ROOT.ML	Wed Jul 01 11:20:32 1998 +0200
     2.2 +++ b/src/HOL/ROOT.ML	Wed Jul 01 11:33:39 1998 +0200
     2.3 @@ -36,7 +36,8 @@
     2.4  use_thy "Ord";
     2.5  use_thy "subset";
     2.6  use "Tools/typedef_package.ML";
     2.7 -use_thy "Inductive";
     2.8 +use_thy "Sum";
     2.9 +use_thy "Gfp";
    2.10  
    2.11  use "Tools/record_package.ML";
    2.12  use_thy "Record";
    2.13 @@ -46,6 +47,7 @@
    2.14  use "arith_data.ML";
    2.15  
    2.16  use "Tools/inductive_package.ML";
    2.17 +use_thy "Inductive";
    2.18  
    2.19  use_thy "RelPow";
    2.20  use_thy "Finite";