src/HOL/HOL.thy
changeset 2552 470bc495373e
parent 2393 651fce76c86c
child 2720 3490ef519a56
equal deleted inserted replaced
2551:fe15e3fcccf0 2552:470bc495373e
   121   "op ~="       :: ['a, 'a] => bool                 (infixl "\\<noteq>" 50)
   121   "op ~="       :: ['a, 'a] => bool                 (infixl "\\<noteq>" 50)
   122   "@Eps"        :: [pttrn, bool] => 'a              ("(3\\<epsilon>_./ _)" [0, 10] 10)
   122   "@Eps"        :: [pttrn, bool] => 'a              ("(3\\<epsilon>_./ _)" [0, 10] 10)
   123   "! "          :: [idts, bool] => bool             ("(3\\<forall>_./ _)" [0, 10] 10)
   123   "! "          :: [idts, bool] => bool             ("(3\\<forall>_./ _)" [0, 10] 10)
   124   "? "          :: [idts, bool] => bool             ("(3\\<exists>_./ _)" [0, 10] 10)
   124   "? "          :: [idts, bool] => bool             ("(3\\<exists>_./ _)" [0, 10] 10)
   125   "?! "         :: [idts, bool] => bool             ("(3\\<exists>!_./ _)" [0, 10] 10)
   125   "?! "         :: [idts, bool] => bool             ("(3\\<exists>!_./ _)" [0, 10] 10)
   126   "@case1"      :: ['a, 'b] => case_syn             ("(2_ \\<mapsto>/ _)" 10)
   126   "@case1"      :: ['a, 'b] => case_syn             ("(2_ \\<Rightarrow>/ _)" 10)
   127 
   127 
   128 syntax (symbols output)
   128 syntax (symbols output)
   129   "*All"        :: [idts, bool] => bool             ("(3\\<forall>_./ _)" [0, 10] 10)
   129   "*All"        :: [idts, bool] => bool             ("(3\\<forall>_./ _)" [0, 10] 10)
   130   "*Ex"         :: [idts, bool] => bool             ("(3\\<exists>_./ _)" [0, 10] 10)
   130   "*Ex"         :: [idts, bool] => bool             ("(3\\<exists>_./ _)" [0, 10] 10)
   131   "*Ex1"        :: [idts, bool] => bool             ("(3\\<exists>!_./ _)" [0, 10] 10)
   131   "*Ex1"        :: [idts, bool] => bool             ("(3\\<exists>!_./ _)" [0, 10] 10)