equal
deleted
inserted
replaced
77 fun id_thm th = |
77 fun id_thm th = |
78 let val {lhs,rhs} = S.dest_eq (#2 (S.strip_forall (#2 (R.dest_thm th)))); |
78 let val {lhs,rhs} = S.dest_eq (#2 (S.strip_forall (#2 (R.dest_thm th)))); |
79 in lhs aconv rhs end |
79 in lhs aconv rhs end |
80 handle U.ERR _ => false; |
80 handle U.ERR _ => false; |
81 |
81 |
82 |
82 val P_imp_P_eq_True = @{thm eqTrueI} RS eq_reflection; |
83 fun prover s = prove_goal @{theory HOL} s (fn _ => [fast_tac HOL_cs 1]); |
|
84 val P_imp_P_iff_True = prover "P --> (P= True)" RS mp; |
|
85 val P_imp_P_eq_True = P_imp_P_iff_True RS eq_reflection; |
|
86 fun mk_meta_eq r = case concl_of r of |
83 fun mk_meta_eq r = case concl_of r of |
87 Const("==",_)$_$_ => r |
84 Const("==",_)$_$_ => r |
88 | _ $(Const("op =",_)$_$_) => r RS eq_reflection |
85 | _ $(Const("op =",_)$_$_) => r RS eq_reflection |
89 | _ => r RS P_imp_P_eq_True |
86 | _ => r RS P_imp_P_eq_True |
90 |
87 |