src/FOL/FOL.ML
changeset 3835 9a5a4e123859
parent 2576 390c9fb786b5
child 4096 8cdf672a83e8
     1.1 --- a/src/FOL/FOL.ML	Fri Oct 10 15:51:38 1997 +0200
     1.2 +++ b/src/FOL/FOL.ML	Fri Oct 10 15:52:12 1997 +0200
     1.3 @@ -22,14 +22,14 @@
     1.4  
     1.5  (*introduction rule involving only EX*)
     1.6  qed_goal "ex_classical" FOL.thy 
     1.7 -   "( ~(EX x. P(x)) ==> P(a)) ==> EX x.P(x)"
     1.8 +   "( ~(EX x. P(x)) ==> P(a)) ==> EX x. P(x)"
     1.9   (fn prems=>
    1.10    [ (rtac classical 1),
    1.11      (eresolve_tac (prems RL [exI]) 1) ]);
    1.12  
    1.13  (*version of above, simplifying ~EX to ALL~ *)
    1.14  qed_goal "exCI" FOL.thy 
    1.15 -   "(ALL x. ~P(x) ==> P(a)) ==> EX x.P(x)"
    1.16 +   "(ALL x. ~P(x) ==> P(a)) ==> EX x. P(x)"
    1.17   (fn [prem]=>
    1.18    [ (rtac ex_classical 1),
    1.19      (resolve_tac [notI RS allI RS prem] 1),