src/FOL/IFOL.thy
changeset 14565 c6dc17aab88a
parent 14236 c73d62ce9d1c
child 14854 61bdf2ae4dc5
--- a/src/FOL/IFOL.thy	Wed Apr 14 13:28:46 2004 +0200
+++ b/src/FOL/IFOL.thy	Wed Apr 14 14:13:05 2004 +0200
@@ -60,6 +60,12 @@
 
 syntax (HTML output)
   Not           :: "o => o"                     ("\<not> _" [40] 40)
+  "op &"        :: "[o, o] => o"                (infixr "\<and>" 35)
+  "op |"        :: "[o, o] => o"                (infixr "\<or>" 30)
+  "ALL "        :: "[idts, o] => o"             ("(3\<forall>_./ _)" [0, 10] 10)
+  "EX "         :: "[idts, o] => o"             ("(3\<exists>_./ _)" [0, 10] 10)
+  "EX! "        :: "[idts, o] => o"             ("(3\<exists>!_./ _)" [0, 10] 10)
+  "_not_equal"  :: "['a, 'a] => o"              (infixl "\<noteq>" 50)
 
 
 local