equal
deleted
inserted
replaced
41 fun mk_meta_eq r = r RS @{thm eq_reflection}; |
41 fun mk_meta_eq r = r RS @{thm eq_reflection}; |
42 fun safe_mk_meta_eq r = mk_meta_eq r handle Thm.THM _ => r; |
42 fun safe_mk_meta_eq r = mk_meta_eq r handle Thm.THM _ => r; |
43 |
43 |
44 fun mk_eq th = case concl_of th |
44 fun mk_eq th = case concl_of th |
45 (*expects Trueprop if not == *) |
45 (*expects Trueprop if not == *) |
46 of Const (@{const_name "=="},_) $ _ $ _ => th |
46 of Const (@{const_name Pure.eq},_) $ _ $ _ => th |
47 | _ $ (Const (@{const_name HOL.eq}, _) $ _ $ _) => mk_meta_eq th |
47 | _ $ (Const (@{const_name HOL.eq}, _) $ _ $ _) => mk_meta_eq th |
48 | _ $ (Const (@{const_name Not}, _) $ _) => th RS @{thm Eq_FalseI} |
48 | _ $ (Const (@{const_name Not}, _) $ _) => th RS @{thm Eq_FalseI} |
49 | _ => th RS @{thm Eq_TrueI} |
49 | _ => th RS @{thm Eq_TrueI} |
50 |
50 |
51 fun mk_eq_True (_: Proof.context) r = |
51 fun mk_eq_True (_: Proof.context) r = |