src/HOL/main.ML
changeset 29249 4dc278c8dc59
parent 29223 e09c53289830
child 29304 5c71a6da989d
equal deleted inserted replaced
29248:f1f1bccf2fc5 29249:4dc278c8dc59
     2     ID:         $Id$
     2     ID:         $Id$
     3  
     3  
     4 Classical Higher-order Logic -- only "Main".
     4 Classical Higher-order Logic -- only "Main".
     5 *)
     5 *)
     6 
     6 
     7 set new_locales;
       
     8 use_thy "Main";
     7 use_thy "Main";