src/FOL/IFOL.thy
changeset 6027 9dd06eeda95c
parent 4854 d1850e0964f2
child 6340 7d5cbd5819a0
     1.1 --- a/src/FOL/IFOL.thy	Fri Dec 11 17:16:23 1998 +0100
     1.2 +++ b/src/FOL/IFOL.thy	Fri Dec 11 18:56:30 1998 +0100
     1.3 @@ -63,6 +63,9 @@
     1.4    "EX! "        :: [idts, o] => o               ("(3\\<exists>!_./ _)" [0, 10] 10)
     1.5    "op ~="       :: ['a, 'a] => o                (infixl "\\<noteq>" 50)
     1.6  
     1.7 +syntax (xsymbols)
     1.8 +  "op -->"      :: [o, o] => o                  (infixr "\\<longrightarrow>" 25)
     1.9 +  "op <->"      :: [o, o] => o                  (infixr "\\<longleftrightarrow>" 25)
    1.10  
    1.11  local
    1.12