src/FOL/IFOL.thy
changeset 3835 9a5a4e123859
parent 2367 eba760ebe315
child 3906 5ae0e1324c56
--- a/src/FOL/IFOL.thy	Fri Oct 10 15:51:38 1997 +0200
+++ b/src/FOL/IFOL.thy	Fri Oct 10 15:52:12 1997 +0200
@@ -96,11 +96,11 @@
 
   (* Quantifiers *)
 
-  allI          "(!!x. P(x)) ==> (ALL x.P(x))"
-  spec          "(ALL x.P(x)) ==> P(x)"
+  allI          "(!!x. P(x)) ==> (ALL x. P(x))"
+  spec          "(ALL x. P(x)) ==> P(x)"
 
-  exI           "P(x) ==> (EX x.P(x))"
-  exE           "[| EX x.P(x);  !!x. P(x) ==> R |] ==> R"
+  exI           "P(x) ==> (EX x. P(x))"
+  exE           "[| EX x. P(x);  !!x. P(x) ==> R |] ==> R"
 
   (* Reflection *)