src/FOL/IFOL.thy
changeset 2205 c5a7c72746ac
parent 1322 9b3d3362a048
child 2257 c8154379738c
     1.1 --- a/src/FOL/IFOL.thy	Mon Nov 18 17:32:38 1996 +0100
     1.2 +++ b/src/FOL/IFOL.thy	Mon Nov 18 17:33:35 1996 +0100
     1.3 @@ -3,7 +3,7 @@
     1.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.5      Copyright   1993  University of Cambridge
     1.6  
     1.7 -Intuitionistic first-order logic
     1.8 +Intuitionistic first-order logic.
     1.9  *)
    1.10  
    1.11  IFOL = Pure +
    1.12 @@ -49,6 +49,17 @@
    1.13  translations
    1.14    "x ~= y"      == "~ (x = y)"
    1.15  
    1.16 +syntax (symbolfont)
    1.17 +  Not           :: o => o                       ("\\{neg} _" [40] 40)
    1.18 +  "op &"        :: [o, o] => o                  (infixr "\\{vee}" 35)
    1.19 +  "op |"        :: [o, o] => o                  (infixr "\\{wedge}" 30)
    1.20 +  "op -->"      :: [o, o] => o                  (infixr "\\{midarrow}\\{rightarrow}" 25)
    1.21 +  "op <->"      :: [o, o] => o                  (infixr "\\{leftarrow}\\{rightarrow}" 25)
    1.22 +  "ALL "        :: [idts, o] => o               ("(3\\{forall}_./ _)" 10)
    1.23 +  "EX "         :: [idts, o] => o               ("(3\\{exists}_./ _)" 10)
    1.24 +  "EX! "        :: [idts, o] => o               ("(3\\{exists}!_./ _)" 10)
    1.25 +  "op ~="       :: ['a, 'a] => o                (infixl "\\{noteq}" 50)
    1.26 +
    1.27  
    1.28  rules
    1.29