hol.thy
changeset 38 7ef6ba42914b
parent 25 5d95fe89f501
child 41 054ce38225b9
equal deleted inserted replaced
37:65a546c2b8ed 38:7ef6ba42914b
    18   term
    18   term
    19 
    19 
    20 types
    20 types
    21   bool 0
    21   bool 0
    22   letbinds, letbind 0
    22   letbinds, letbind 0
       
    23   case_syn,cases_syn 0
    23 
    24 
    24 arities
    25 arities
    25   fun :: (term, term) term
    26   fun :: (term, term) term
    26   bool :: term
    27   bool :: term
    27 
    28 
    46   Let           :: "['a, 'a => 'b] => 'b"
    47   Let           :: "['a, 'a => 'b] => 'b"
    47   "_bind"       :: "[idt, 'a] => letbind"             ("(2_ =/ _)" 10)
    48   "_bind"       :: "[idt, 'a] => letbind"             ("(2_ =/ _)" 10)
    48   ""            :: "letbind => letbinds"              ("_")
    49   ""            :: "letbind => letbinds"              ("_")
    49   "_binds"      :: "[letbind, letbinds] => letbinds"  ("_;/ _")
    50   "_binds"      :: "[letbind, letbinds] => letbinds"  ("_;/ _")
    50   "_Let"        :: "[letbinds, 'a] => 'a"            ("(let (_)/ in (_))" 10)
    51   "_Let"        :: "[letbinds, 'a] => 'a"            ("(let (_)/ in (_))" 10)
       
    52 
       
    53   (* Case expressions *)
       
    54 
       
    55   "@case"            :: "['a, cases_syn] => 'b"		("(case _ of/ _)" 10)
       
    56   "@case1"           :: "['a, 'b] => case_syn"		("(2_ =>/ _)" 10)
       
    57   ""                 :: "case_syn => cases_syn"		("_")
       
    58   "@case2"           :: "[case_syn,cases_syn] => cases_syn"	("_/ | _")
    51 
    59 
    52   (* Alternative Quantifiers *)
    60   (* Alternative Quantifiers *)
    53 
    61 
    54   "*All"        :: "[idts, bool] => bool"             ("(3ALL _./ _)" 10)
    62   "*All"        :: "[idts, bool] => bool"             ("(3ALL _./ _)" 10)
    55   "*Ex"         :: "[idts, bool] => bool"             ("(3EX _./ _)" 10)
    63   "*Ex"         :: "[idts, bool] => bool"             ("(3EX _./ _)" 10)