src/FOL/IFOL.thy
changeset 3906 5ae0e1324c56
parent 3835 9a5a4e123859
child 3932 436463f9f2b4
     1.1 --- a/src/FOL/IFOL.thy	Thu Oct 16 15:31:12 1997 +0200
     1.2 +++ b/src/FOL/IFOL.thy	Thu Oct 16 15:33:06 1997 +0200
     1.3 @@ -8,6 +8,8 @@
     1.4  
     1.5  IFOL = Pure +
     1.6  
     1.7 +global
     1.8 +
     1.9  classes
    1.10    term < logic
    1.11  
    1.12 @@ -62,6 +64,8 @@
    1.13    "op ~="       :: ['a, 'a] => o                (infixl "\\<noteq>" 50)
    1.14  
    1.15  
    1.16 +path IFOL
    1.17 +
    1.18  rules
    1.19  
    1.20    (* Equality *)
    1.21 @@ -108,4 +112,3 @@
    1.22    iff_reflection  "(P<->Q) ==> (P==Q)"
    1.23  
    1.24  end
    1.25 -