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 *)