# HG changeset patch
# User wenzelm
# Date 848334815 -3600
# Node ID c5a7c72746ac9bf3f0a7e2a15269bed84fc63b6a
# Parent  64cb98f841e4becb6416a4e213337e1b9437ad63
added symbolfont syntax;

diff -r 64cb98f841e4 -r c5a7c72746ac src/FOL/IFOL.thy
--- a/src/FOL/IFOL.thy	Mon Nov 18 17:32:38 1996 +0100
+++ b/src/FOL/IFOL.thy	Mon Nov 18 17:33:35 1996 +0100
@@ -3,7 +3,7 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
-Intuitionistic first-order logic
+Intuitionistic first-order logic.
 *)
 
 IFOL = Pure +
@@ -49,6 +49,17 @@
 translations
   "x ~= y"      == "~ (x = y)"
 
+syntax (symbolfont)
+  Not           :: o => o                       ("\\{neg} _" [40] 40)
+  "op &"        :: [o, o] => o                  (infixr "\\{vee}" 35)
+  "op |"        :: [o, o] => o                  (infixr "\\{wedge}" 30)
+  "op -->"      :: [o, o] => o                  (infixr "\\{midarrow}\\{rightarrow}" 25)
+  "op <->"      :: [o, o] => o                  (infixr "\\{leftarrow}\\{rightarrow}" 25)
+  "ALL "        :: [idts, o] => o               ("(3\\{forall}_./ _)" 10)
+  "EX "         :: [idts, o] => o               ("(3\\{exists}_./ _)" 10)
+  "EX! "        :: [idts, o] => o               ("(3\\{exists}!_./ _)" 10)
+  "op ~="       :: ['a, 'a] => o                (infixl "\\{noteq}" 50)
+
 
 rules