equal
deleted
inserted
replaced
65 handle U.ERR _ => false; |
65 handle U.ERR _ => false; |
66 |
66 |
67 val P_imp_P_eq_True = @{thm eqTrueI} RS eq_reflection; |
67 val P_imp_P_eq_True = @{thm eqTrueI} RS eq_reflection; |
68 fun mk_meta_eq r = case concl_of r of |
68 fun mk_meta_eq r = case concl_of r of |
69 Const("==",_)$_$_ => r |
69 Const("==",_)$_$_ => r |
70 | _ $(Const(@{const_name "op ="},_)$_$_) => r RS eq_reflection |
70 | _ $(Const(@{const_name HOL.eq},_)$_$_) => r RS eq_reflection |
71 | _ => r RS P_imp_P_eq_True |
71 | _ => r RS P_imp_P_eq_True |
72 |
72 |
73 (*Is this the best way to invoke the simplifier??*) |
73 (*Is this the best way to invoke the simplifier??*) |
74 fun rewrite L = rewrite_rule (map mk_meta_eq (filter_out id_thm L)) |
74 fun rewrite L = rewrite_rule (map mk_meta_eq (filter_out id_thm L)) |
75 |
75 |