equal
deleted
inserted
replaced
48 | _ $ (Const (@{const_name HOL.eq}, _) $ _ $ _) => mk_meta_eq th |
48 | _ $ (Const (@{const_name HOL.eq}, _) $ _ $ _) => mk_meta_eq th |
49 | _ $ (Const (@{const_name Not}, _) $ _) => th RS @{thm Eq_FalseI} |
49 | _ $ (Const (@{const_name Not}, _) $ _) => th RS @{thm Eq_FalseI} |
50 | _ => th RS @{thm Eq_TrueI}) |
50 | _ => th RS @{thm Eq_TrueI}) |
51 |
51 |
52 fun mk_eq_True (_: Proof.context) r = |
52 fun mk_eq_True (_: Proof.context) r = |
53 SOME (r RS @{thm meta_eq_to_obj_eq} RS @{thm Eq_TrueI}) handle Thm.THM _ => NONE; |
53 SOME (HOLogic.mk_obj_eq r RS @{thm Eq_TrueI}) handle Thm.THM _ => NONE; |
54 |
54 |
55 (* Produce theorems of the form |
55 (* Produce theorems of the form |
56 (P1 =simp=> ... =simp=> Pn => x == y) ==> (P1 =simp=> ... =simp=> Pn => x = y) |
56 (P1 =simp=> ... =simp=> Pn => x == y) ==> (P1 =simp=> ... =simp=> Pn => x = y) |
57 *) |
57 *) |
58 |
58 |