--- a/src/FOL/IFOL.thy Wed Oct 15 11:02:28 2003 +0200
+++ b/src/FOL/IFOL.thy Thu Oct 16 10:31:40 2003 +0200
@@ -64,6 +64,13 @@
local
+finalconsts
+ False All Ex
+ "op ="
+ "op &"
+ "op |"
+ "op -->"
+
axioms
(* Equality *)
@@ -86,18 +93,6 @@
FalseE: "False ==> P"
-
- (* Definitions *)
-
- True_def: "True == False-->False"
- not_def: "~P == P-->False"
- iff_def: "P<->Q == (P-->Q) & (Q-->P)"
-
- (* Unique existence *)
-
- ex1_def: "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)"
-
-
(* Quantifiers *)
allI: "(!!x. P(x)) ==> (ALL x. P(x))"
@@ -112,6 +107,17 @@
iff_reflection: "(P<->Q) ==> (P==Q)"
+defs
+ (* Definitions *)
+
+ True_def: "True == False-->False"
+ not_def: "~P == P-->False"
+ iff_def: "P<->Q == (P-->Q) & (Q-->P)"
+
+ (* Unique existence *)
+
+ ex1_def: "Ex1(P) == EX x. P(x) & (ALL y. P(y) --> y=x)"
+
subsection {* Lemmas and proof tools *}