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