src/HOL/HOL.thy
changeset 3248 3e1664348551
parent 3230 3772723c5e41
child 3320 3a5e4930fb77
equal deleted inserted replaced
3247:067dc2d07489 3248:3e1664348551
   114   "_Let (_binds b bs) e"  == "_Let b (_Let bs e)"
   114   "_Let (_binds b bs) e"  == "_Let b (_Let bs e)"
   115   "let x = a in e"        == "Let a (%x. e)"
   115   "let x = a in e"        == "Let a (%x. e)"
   116 
   116 
   117 syntax (symbols output)
   117 syntax (symbols output)
   118   "op ~="       :: ['a, 'a] => bool                 ("(_ \\<noteq>/ _)" [51, 51] 50)
   118   "op ~="       :: ['a, 'a] => bool                 ("(_ \\<noteq>/ _)" [51, 51] 50)
       
   119   "*All"        :: [idts, bool] => bool             ("(3\\<forall>_./ _)" [0, 10] 10)
       
   120   "*Ex"         :: [idts, bool] => bool             ("(3\\<exists>_./ _)" [0, 10] 10)
       
   121   "*Ex1"        :: [idts, bool] => bool             ("(3\\<exists>!_./ _)" [0, 10] 10)
   119 
   122 
   120 syntax (symbols)
   123 syntax (symbols)
   121   Not           :: bool => bool                     ("\\<not> _" [40] 40)
   124   Not           :: bool => bool                     ("\\<not> _" [40] 40)
   122   "op &"        :: [bool, bool] => bool             (infixr "\\<and>" 35)
   125   "op &"        :: [bool, bool] => bool             (infixr "\\<and>" 35)
   123   "op |"        :: [bool, bool] => bool             (infixr "\\<or>" 30)
   126   "op |"        :: [bool, bool] => bool             (infixr "\\<or>" 30)
   128   "! "          :: [idts, bool] => bool             ("(3\\<forall>_./ _)" [0, 10] 10)
   131   "! "          :: [idts, bool] => bool             ("(3\\<forall>_./ _)" [0, 10] 10)
   129   "? "          :: [idts, bool] => bool             ("(3\\<exists>_./ _)" [0, 10] 10)
   132   "? "          :: [idts, bool] => bool             ("(3\\<exists>_./ _)" [0, 10] 10)
   130   "?! "         :: [idts, bool] => bool             ("(3\\<exists>!_./ _)" [0, 10] 10)
   133   "?! "         :: [idts, bool] => bool             ("(3\\<exists>!_./ _)" [0, 10] 10)
   131   "@case1"      :: ['a, 'b] => case_syn             ("(2_ \\<Rightarrow>/ _)" 10)
   134   "@case1"      :: ['a, 'b] => case_syn             ("(2_ \\<Rightarrow>/ _)" 10)
   132 (*"@case2"      :: [case_syn, cases_syn] => cases_syn   ("_/ \\<orelse> _")*)
   135 (*"@case2"      :: [case_syn, cases_syn] => cases_syn   ("_/ \\<orelse> _")*)
   133 
       
   134 syntax (symbols output)
       
   135   "*All"        :: [idts, bool] => bool             ("(3\\<forall>_./ _)" [0, 10] 10)
       
   136   "*Ex"         :: [idts, bool] => bool             ("(3\\<exists>_./ _)" [0, 10] 10)
       
   137   "*Ex1"        :: [idts, bool] => bool             ("(3\\<exists>!_./ _)" [0, 10] 10)
       
   138 
       
   139 
   136 
   140 
   137 
   141 
   138 
   142 (** Rules and definitions **)
   139 (** Rules and definitions **)
   143 
   140