src/FOL/IFOL.thy
changeset 14236 c73d62ce9d1c
parent 13779 2a34dc5cf79e
child 14565 c6dc17aab88a
     1.1 --- a/src/FOL/IFOL.thy	Wed Oct 15 11:02:28 2003 +0200
     1.2 +++ b/src/FOL/IFOL.thy	Thu Oct 16 10:31:40 2003 +0200
     1.3 @@ -64,6 +64,13 @@
     1.4  
     1.5  local
     1.6  
     1.7 +finalconsts
     1.8 +  False All Ex
     1.9 +  "op ="
    1.10 +  "op &"
    1.11 +  "op |"
    1.12 +  "op -->"
    1.13 +
    1.14  axioms
    1.15  
    1.16    (* Equality *)
    1.17 @@ -86,18 +93,6 @@
    1.18  
    1.19    FalseE:       "False ==> P"
    1.20  
    1.21 -
    1.22 -  (* Definitions *)
    1.23 -
    1.24 -  True_def:     "True  == False-->False"
    1.25 -  not_def:      "~P    == P-->False"
    1.26 -  iff_def:      "P<->Q == (P-->Q) & (Q-->P)"
    1.27 -
    1.28 -  (* Unique existence *)
    1.29 -
    1.30 -  ex1_def:      "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)"
    1.31 -
    1.32 -
    1.33    (* Quantifiers *)
    1.34  
    1.35    allI:         "(!!x. P(x)) ==> (ALL x. P(x))"
    1.36 @@ -112,6 +107,17 @@
    1.37    iff_reflection: "(P<->Q) ==> (P==Q)"
    1.38  
    1.39  
    1.40 +defs
    1.41 +  (* Definitions *)
    1.42 +
    1.43 +  True_def:     "True  == False-->False"
    1.44 +  not_def:      "~P    == P-->False"
    1.45 +  iff_def:      "P<->Q == (P-->Q) & (Q-->P)"
    1.46 +
    1.47 +  (* Unique existence *)
    1.48 +
    1.49 +  ex1_def:      "Ex1(P) == EX x. P(x) & (ALL y. P(y) --> y=x)"
    1.50 +
    1.51  
    1.52  subsection {* Lemmas and proof tools *}
    1.53