changeset 14765 | bafb24c150c1 |
parent 3837 | d7f033c74b38 |
child 17456 | bcf7544875b2 |
--- a/src/CCL/Term.thy Wed May 19 11:41:58 2004 +0200 +++ b/src/CCL/Term.thy Fri May 21 21:14:18 2004 +0200 @@ -37,6 +37,7 @@ letrec2 :: "[[i,i,i=>i=>i]=>i,(i=>i=>i)=>i]=>i" letrec3 :: "[[i,i,i,i=>i=>i=>i]=>i,(i=>i=>i=>i)=>i]=>i" +syntax "@let" :: "[idt,i,i]=>i" ("(3let _ be _/ in _)" [0,0,60] 60) @@ -49,6 +50,7 @@ "@letrec3" :: "[idt,idt,idt,idt,i,i]=>i" ("(3letrec _ _ _ _ be _/ in _)" [0,0,0,0,0,60] 60) +consts napply :: "[i=>i,i,i]=>i" ("(_ ^ _ ` _)" [56,56,56] 56) rules