src/CCL/Term.thy
changeset 610 ede55dd46f9d
parent 289 78541329ff35
child 998 91d09e262799
equal deleted inserted replaced
609:6d520505e704 610:ede55dd46f9d
    35   let        ::       "[i,i=>i]=>i"
    35   let        ::       "[i,i=>i]=>i"
    36   letrec     ::       "[[i,i=>i]=>i,(i=>i)=>i]=>i"
    36   letrec     ::       "[[i,i=>i]=>i,(i=>i)=>i]=>i"
    37   letrec2    ::       "[[i,i,i=>i=>i]=>i,(i=>i=>i)=>i]=>i"
    37   letrec2    ::       "[[i,i,i=>i=>i]=>i,(i=>i=>i)=>i]=>i"
    38   letrec3    ::       "[[i,i,i,i=>i=>i=>i]=>i,(i=>i=>i=>i)=>i]=>i"  
    38   letrec3    ::       "[[i,i,i,i=>i=>i=>i]=>i,(i=>i=>i=>i)=>i]=>i"  
    39 
    39 
    40   "@let"     ::       "[id,i,i]=>i"             ("(3let _ be _/ in _)" [] 60)
    40   "@let"     ::       "[idt,i,i]=>i"             ("(3let _ be _/ in _)" [] 60)
    41   "@letrec"  ::       "[id,id,i,i]=>i"          ("(3letrec _ _ be _/ in _)"  [] 60)
    41   "@letrec"  ::       "[idt,idt,i,i]=>i"          ("(3letrec _ _ be _/ in _)"  [] 60)
    42   "@letrec2" ::       "[id,id,id,i,i]=>i"       ("(3letrec _ _ _ be _/ in _)"  [] 60)
    42   "@letrec2" ::       "[idt,idt,idt,i,i]=>i"       ("(3letrec _ _ _ be _/ in _)"  [] 60)
    43   "@letrec3" ::       "[id,id,id,id,i,i]=>i"    ("(3letrec _ _ _ _ be _/ in _)"  [] 60)
    43   "@letrec3" ::       "[idt,idt,idt,idt,i,i]=>i"    ("(3letrec _ _ _ _ be _/ in _)"  [] 60)
    44 
    44 
    45   napply    :: "[i=>i,i,i]=>i"      ("(_ ^ _ ` _)")
    45   napply    :: "[i=>i,i,i]=>i"      ("(_ ^ _ ` _)")
    46 
    46 
    47 rules
    47 rules
    48 
    48