Gave tighter priorities to if, napply and the let-forms to
authorlcp
Thu Apr 06 10:51:42 1995 +0200 (1995-04-06)
changeset 99891d09e262799
parent 997 a58082b8066c
child 999 9bf3816298d0
Gave tighter priorities to if, napply and the let-forms to
reduce ambiguities.
src/CCL/Term.thy
     1.1 --- a/src/CCL/Term.thy	Thu Apr 06 10:49:53 1995 +0200
     1.2 +++ b/src/CCL/Term.thy	Thu Apr 06 10:51:42 1995 +0200
     1.3 @@ -11,38 +11,45 @@
     1.4  
     1.5  consts
     1.6  
     1.7 -  one        ::	      "i"
     1.8 +  one        :: "i"
     1.9  
    1.10 -  if         ::       "[i,i,i]=>i"           ("(3if _/ then _/ else _)" [] 60)
    1.11 +  if         :: "[i,i,i]=>i"           ("(3if _/ then _/ else _)" [0,0,60] 60)
    1.12  
    1.13 -  inl,inr    ::	      "i=>i"
    1.14 -  when       ::	      "[i,i=>i,i=>i]=>i" 
    1.15 +  inl,inr    :: "i=>i"
    1.16 +  when       :: "[i,i=>i,i=>i]=>i" 
    1.17  
    1.18 -  split      ::	      "[i,[i,i]=>i]=>i"
    1.19 +  split      :: "[i,[i,i]=>i]=>i"
    1.20    fst,snd,   
    1.21 -  thd        ::       "i=>i"
    1.22 +  thd        :: "i=>i"
    1.23  
    1.24 -  zero       ::	      "i"
    1.25 -  succ       ::	      "i=>i"
    1.26 -  ncase      ::	      "[i,i,i=>i]=>i"
    1.27 -  nrec       ::	      "[i,i,[i,i]=>i]=>i"
    1.28 +  zero       :: "i"
    1.29 +  succ       :: "i=>i"
    1.30 +  ncase      :: "[i,i,i=>i]=>i"
    1.31 +  nrec       :: "[i,i,[i,i]=>i]=>i"
    1.32  
    1.33 -  nil        ::       "i"                    ("([])")
    1.34 -  "$"        ::       "[i,i]=>i"             (infixr 80)
    1.35 -  lcase      ::	      "[i,i,[i,i]=>i]=>i"
    1.36 -  lrec       ::	      "[i,i,[i,i,i]=>i]=>i"
    1.37 +  nil        :: "i"                        ("([])")
    1.38 +  "$"        :: "[i,i]=>i"                 (infixr 80)
    1.39 +  lcase      :: "[i,i,[i,i]=>i]=>i"
    1.40 +  lrec       :: "[i,i,[i,i,i]=>i]=>i"
    1.41 +
    1.42 +  let        :: "[i,i=>i]=>i"
    1.43 +  letrec     :: "[[i,i=>i]=>i,(i=>i)=>i]=>i"
    1.44 +  letrec2    :: "[[i,i,i=>i=>i]=>i,(i=>i=>i)=>i]=>i"
    1.45 +  letrec3    :: "[[i,i,i,i=>i=>i=>i]=>i,(i=>i=>i=>i)=>i]=>i"  
    1.46  
    1.47 -  let        ::       "[i,i=>i]=>i"
    1.48 -  letrec     ::       "[[i,i=>i]=>i,(i=>i)=>i]=>i"
    1.49 -  letrec2    ::       "[[i,i,i=>i=>i]=>i,(i=>i=>i)=>i]=>i"
    1.50 -  letrec3    ::       "[[i,i,i,i=>i=>i=>i]=>i,(i=>i=>i=>i)=>i]=>i"  
    1.51 +  "@let"     :: "[idt,i,i]=>i"             ("(3let _ be _/ in _)"
    1.52 +  			[0,0,60] 60)
    1.53 +
    1.54 +  "@letrec"  :: "[idt,idt,i,i]=>i"         ("(3letrec _ _ be _/ in _)"
    1.55 +  			[0,0,0,60] 60)
    1.56  
    1.57 -  "@let"     ::       "[idt,i,i]=>i"             ("(3let _ be _/ in _)" [] 60)
    1.58 -  "@letrec"  ::       "[idt,idt,i,i]=>i"          ("(3letrec _ _ be _/ in _)"  [] 60)
    1.59 -  "@letrec2" ::       "[idt,idt,idt,i,i]=>i"       ("(3letrec _ _ _ be _/ in _)"  [] 60)
    1.60 -  "@letrec3" ::       "[idt,idt,idt,idt,i,i]=>i"    ("(3letrec _ _ _ _ be _/ in _)"  [] 60)
    1.61 +  "@letrec2" :: "[idt,idt,idt,i,i]=>i"     ("(3letrec _ _ _ be _/ in _)"
    1.62 +  			[0,0,0,0,60] 60)
    1.63  
    1.64 -  napply    :: "[i=>i,i,i]=>i"      ("(_ ^ _ ` _)")
    1.65 +  "@letrec3" :: "[idt,idt,idt,idt,i,i]=>i" ("(3letrec _ _ _ _ be _/ in _)"
    1.66 +  			[0,0,0,0,0,60] 60)
    1.67 +
    1.68 +  napply     :: "[i=>i,i,i]=>i"            ("(_ ^ _ ` _)" [56,56,56] 56)
    1.69  
    1.70  rules
    1.71