TFL/rules.new.sml
changeset 3272 c93f54759539
parent 3245 241838c01caf
child 3302 404fe31fd8d2
equal deleted inserted replaced
3271:b873969b05d3 3272:c93f54759539
   399 val simplify = rewrite_rule;
   399 val simplify = rewrite_rule;
   400 
   400 
   401 local fun rew_conv mss = rewrite_cterm (true,false) mss (K(K None))
   401 local fun rew_conv mss = rewrite_cterm (true,false) mss (K(K None))
   402 in
   402 in
   403 fun simpl_conv thl ctm = 
   403 fun simpl_conv thl ctm = 
   404  rew_conv (Thm.mss_of (#simps(rep_ss HOL_ss)@thl)) ctm
   404  rew_conv (Thm.mss_of (#simps(rep_ss (!simpset))@thl)) ctm
   405  RS meta_eq_to_obj_eq
   405  RS meta_eq_to_obj_eq
   406 end;
   406 end;
   407 
   407 
   408 local fun prover s = prove_goal HOL.thy s (fn _ => [fast_tac HOL_cs 1])
   408 local fun prover s = prove_goal HOL.thy s (fn _ => [fast_tac HOL_cs 1])
   409 in
   409 in
   529 val term_ref = ref[] : term list ref
   529 val term_ref = ref[] : term list ref
   530 val mss_ref = ref [] : meta_simpset list ref;
   530 val mss_ref = ref [] : meta_simpset list ref;
   531 val thm_ref = ref [] : thm list ref;
   531 val thm_ref = ref [] : thm list ref;
   532 val tracing = ref false;
   532 val tracing = ref false;
   533 
   533 
   534 fun say s = if !tracing then (output(std_out,s); flush_out std_out) else ();
   534 fun say s = if !tracing then TextIO.output (TextIO.stdOut, s) else ();
   535 
   535 
   536 fun print_thms s L = 
   536 fun print_thms s L = 
   537    (say s; 
   537    (say s; 
   538     map (fn th => say (string_of_thm th ^"\n")) L;
   538     map (fn th => say (string_of_thm th ^"\n")) L;
   539     say"\n");
   539     say"\n");