src/HOL/HOL.ML
changeset 4087 42229596565c
parent 4025 77e426be5624
child 4131 916641b59219
equal deleted inserted replaced
4086:958806f7e840 4087:42229596565c
   372 
   372 
   373 fun qed_goalw_spec_mp name thy defs s p = 
   373 fun qed_goalw_spec_mp name thy defs s p = 
   374 	bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goalw thy defs s p));
   374 	bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goalw thy defs s p));
   375 
   375 
   376 end;
   376 end;
   377 
       
   378 
       
   379 (*Thus, assignments to the references claset and simpset are recorded
       
   380   with theory "HOL".  These files cannot be loaded directly in ROOT.ML.*)
       
   381 use "hologic.ML";
       
   382 use "cladata.ML";
       
   383 use "simpdata.ML";