src/HOL/ROOT.ML
changeset 5124 1ce3cccfacdb
parent 5110 2497807020fa
child 5183 89f162de39cf
     1.1 --- a/src/HOL/ROOT.ML	Fri Jul 03 17:34:55 1998 +0200
     1.2 +++ b/src/HOL/ROOT.ML	Fri Jul 03 17:35:39 1998 +0200
     1.3 @@ -52,7 +52,7 @@
     1.4  use_thy "RelPow";
     1.5  use_thy "Finite";
     1.6  use_thy "Sexp";
     1.7 -use_thy "WF_Rel";
     1.8 +use_thy "Recdef";
     1.9  use_thy "Map";
    1.10  use_thy "Update";
    1.11  
    1.12 @@ -65,6 +65,9 @@
    1.13  use "sys.sml";
    1.14  cd "$ISABELLE_HOME/src/HOL";
    1.15  
    1.16 +(*the all-in-one theory*)
    1.17 +use_thy "Main";
    1.18 +
    1.19  print_depth 8;
    1.20  
    1.21  val HOL_build_completed = ();   (*indicate successful build*)