src/CCL/Term.thy
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