src/Sequents/LK0.thy
changeset 14565 c6dc17aab88a
parent 12662 a9bbba3473f3
child 14765 bafb24c150c1
     1.1 --- a/src/Sequents/LK0.thy	Wed Apr 14 13:28:46 2004 +0200
     1.2 +++ b/src/Sequents/LK0.thy	Wed Apr 14 14:13:05 2004 +0200
     1.3 @@ -53,6 +53,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