equal
deleted
inserted
replaced
69 Const("==",_)$_$_ => r |
69 Const("==",_)$_$_ => r |
70 | _ $(Const("op =",_)$_$_) => r RS eq_reflection |
70 | _ $(Const("op =",_)$_$_) => 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 (List.filter(not o id_thm) L)) |
74 fun rewrite L = rewrite_rule (map mk_meta_eq (filter_out id_thm L)) |
75 |
75 |
76 fun join_assums th = |
76 fun join_assums th = |
77 let val thy = Thm.theory_of_thm th |
77 let val thy = Thm.theory_of_thm th |
78 val tych = cterm_of thy |
78 val tych = cterm_of thy |
79 val {lhs,rhs} = S.dest_eq(#2 (S.strip_forall (concl th))) |
79 val {lhs,rhs} = S.dest_eq(#2 (S.strip_forall (concl th))) |