src/HOL/main.ML
changeset 29223 e09c53289830
parent 28401 d5f39173444c
child 29249 4dc278c8dc59
equal deleted inserted replaced
29208:b0c81b9a0133 29223:e09c53289830
     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;
     7 use_thy "Main";
     8 use_thy "Main";