src/Sequents/simpdata.ML
changeset 9259 103acc345f75
parent 7570 a9391550eea1
child 9713 2c5b42311eb0
--- a/src/Sequents/simpdata.ML	Thu Jul 06 11:23:39 2000 +0200
+++ b/src/Sequents/simpdata.ML	Thu Jul 06 11:24:09 2000 +0200
@@ -104,12 +104,18 @@
  | _ => [r];
 
 
-qed_goal "P_iff_F" LK.thy "|- ~P ==> |- (P <-> False)"
-    (fn prems => [lemma_tac (hd prems) 1, fast_tac LK_pack 1]);
+Goal "|- ~P ==> |- (P <-> False)";
+by (etac (thinR RS cut) 1);
+by (Fast_tac 1);		
+qed "P_iff_F";
+
 val iff_reflection_F = P_iff_F RS iff_reflection;
 
-qed_goal "P_iff_T" LK.thy "|- P ==> |- (P <-> True)"
-    (fn prems => [lemma_tac (hd prems) 1, fast_tac LK_pack 1]);
+Goal "|- P ==> |- (P <-> True)";
+by (etac (thinR RS cut) 1);
+by (Fast_tac 1);		
+qed "P_iff_T";
+
 val iff_reflection_T = P_iff_T RS iff_reflection;
 
 (*Make meta-equalities.*)