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