equal
deleted
inserted
replaced
391 rewrite_rule (map (fn th => (th RS eq_reflection) handle _ => th) thl); |
391 rewrite_rule (map (fn th => (th RS eq_reflection) handle _ => th) thl); |
392 |
392 |
393 local fun rew_conv mss = rewrite_cterm (true,false) mss (K(K None)) |
393 local fun rew_conv mss = rewrite_cterm (true,false) mss (K(K None)) |
394 in |
394 in |
395 fun simpl_conv ss thl ctm = |
395 fun simpl_conv ss thl ctm = |
396 rew_conv (Thm.mss_of (#simps(rep_ss ss)@thl)) ctm |
396 rew_conv (Thm.mss_of (#simps (Thm.dest_mss (#mss (rep_ss ss))) @ thl)) ctm |
397 RS meta_eq_to_obj_eq |
397 RS meta_eq_to_obj_eq |
398 end; |
398 end; |
399 |
399 |
400 local fun prover s = prove_goal HOL.thy s (fn _ => [fast_tac HOL_cs 1]) |
400 local fun prover s = prove_goal HOL.thy s (fn _ => [fast_tac HOL_cs 1]) |
401 in |
401 in |