equal
deleted
inserted
replaced
102 | _ => [r]) |
102 | _ => [r]) |
103 | _ => []) (*ignore theorem unless it has precisely one conclusion*) |
103 | _ => []) (*ignore theorem unless it has precisely one conclusion*) |
104 | _ => [r]; |
104 | _ => [r]; |
105 |
105 |
106 |
106 |
107 qed_goal "P_iff_F" LK.thy "|- ~P ==> |- (P <-> False)" |
107 Goal "|- ~P ==> |- (P <-> False)"; |
108 (fn prems => [lemma_tac (hd prems) 1, fast_tac LK_pack 1]); |
108 by (etac (thinR RS cut) 1); |
|
109 by (Fast_tac 1); |
|
110 qed "P_iff_F"; |
|
111 |
109 val iff_reflection_F = P_iff_F RS iff_reflection; |
112 val iff_reflection_F = P_iff_F RS iff_reflection; |
110 |
113 |
111 qed_goal "P_iff_T" LK.thy "|- P ==> |- (P <-> True)" |
114 Goal "|- P ==> |- (P <-> True)"; |
112 (fn prems => [lemma_tac (hd prems) 1, fast_tac LK_pack 1]); |
115 by (etac (thinR RS cut) 1); |
|
116 by (Fast_tac 1); |
|
117 qed "P_iff_T"; |
|
118 |
113 val iff_reflection_T = P_iff_T RS iff_reflection; |
119 val iff_reflection_T = P_iff_T RS iff_reflection; |
114 |
120 |
115 (*Make meta-equalities.*) |
121 (*Make meta-equalities.*) |
116 fun mk_meta_eq th = case concl_of th of |
122 fun mk_meta_eq th = case concl_of th of |
117 Const("==",_)$_$_ => th |
123 Const("==",_)$_$_ => th |