src/Sequents/LK0.ML
changeset 9259 103acc345f75
parent 7122 87b233b31889
child 17481 75166ebb619b
     1.1 --- a/src/Sequents/LK0.ML	Thu Jul 06 11:23:39 2000 +0200
     1.2 +++ b/src/Sequents/LK0.ML	Thu Jul 06 11:24:09 2000 +0200
     1.3 @@ -149,15 +149,20 @@
     1.4  by (rtac thinR 1 THEN rtac prem 1);
     1.5  qed "backwards_impR";
     1.6  
     1.7 - 
     1.8 -qed_goal "conjunct1" thy "|-P&Q ==> |-P"
     1.9 -    (fn [major] => [lemma_tac major 1,  Fast_tac 1]);
    1.10 +Goal "|-P&Q ==> |-P";
    1.11 +by (etac (thinR RS cut) 1);
    1.12 +by (Fast_tac 1);		
    1.13 +qed "conjunct1";
    1.14  
    1.15 -qed_goal "conjunct2" thy "|-P&Q ==> |-Q"
    1.16 -    (fn [major] => [lemma_tac major 1,  Fast_tac 1]);
    1.17 +Goal "|-P&Q ==> |-Q";
    1.18 +by (etac (thinR RS cut) 1);
    1.19 +by (Fast_tac 1);		
    1.20 +qed "conjunct2";
    1.21  
    1.22 -qed_goal "spec" thy "|- (ALL x. P(x)) ==> |- P(x)"
    1.23 -    (fn [major] => [lemma_tac major 1,  Fast_tac 1]);
    1.24 +Goal "|- (ALL x. P(x)) ==> |- P(x)";
    1.25 +by (etac (thinR RS cut) 1);
    1.26 +by (Fast_tac 1);		
    1.27 +qed "spec";
    1.28  
    1.29  (** Equality **)
    1.30