equal
deleted
inserted
replaced
27 | _ => []) (*ignore theorem unless it has precisely one conclusion*) |
27 | _ => []) (*ignore theorem unless it has precisely one conclusion*) |
28 | _ => [r]; |
28 | _ => [r]; |
29 |
29 |
30 (*Make meta-equalities.*) |
30 (*Make meta-equalities.*) |
31 fun mk_meta_eq ctxt th = case concl_of th of |
31 fun mk_meta_eq ctxt th = case concl_of th of |
32 Const("==",_)$_$_ => th |
32 Const(@{const_name Pure.eq},_)$_$_ => th |
33 | Const(@{const_name Trueprop},_) $ Abs(_,_,a) $ Abs(_,_,c) => |
33 | Const(@{const_name Trueprop},_) $ Abs(_,_,a) $ Abs(_,_,c) => |
34 (case (Cla.forms_of_seq a, Cla.forms_of_seq c) of |
34 (case (Cla.forms_of_seq a, Cla.forms_of_seq c) of |
35 ([], [p]) => |
35 ([], [p]) => |
36 (case p of |
36 (case p of |
37 (Const(@{const_name equal},_)$_$_) => th RS @{thm eq_reflection} |
37 (Const(@{const_name equal},_)$_$_) => th RS @{thm eq_reflection} |