src/HOL/Import/HOL/ROOT.ML
changeset 17644 bd59bfd4bf37
parent 15647 b1f486a9c56b
child 17648 7568d2cc560e
     1.1 --- a/src/HOL/Import/HOL/ROOT.ML	Mon Sep 26 02:06:44 2005 +0200
     1.2 +++ b/src/HOL/Import/HOL/ROOT.ML	Mon Sep 26 02:27:14 2005 +0200
     1.3 @@ -3,5 +3,6 @@
     1.4      Author:     Sebastian Skalberg (TU Muenchen)
     1.5  *)
     1.6  
     1.7 -setmp quick_and_dirty true use_thy "HOL4Prob";
     1.8 -setmp quick_and_dirty true use_thy "HOL4";
     1.9 +set show_types; set show_sorts;
    1.10 +use_thy "HOL4Prob";
    1.11 +use_thy "HOL4";