src/HOL/Import/ROOT.ML
changeset 37296 1fad5b94c0ae
parent 25374 7657a081fcb4
equal deleted inserted replaced
37295:5c0499f4f4c8 37296:1fad5b94c0ae
     1 (*  Title:      HOL/Import/ROOT.ML
     1 (*  Title:      HOL/Import/ROOT.ML
     2     ID:         $Id$
       
     3     Author:     Sebastian Skalberg (TU Muenchen)
     2     Author:     Sebastian Skalberg (TU Muenchen)
     4 *)
     3 *)
     5 
     4 
     6 Proofterm.proofs := 0;
     5 use_thys ["HOL4Compat", "HOL4Syntax"];
     7 use_thy "HOL4Compat";
       
     8 use_thy "HOL4Syntax";