src/FOLP/IFOLP.thy
changeset 648 e27c9ec2b48b
parent 283 76caebd18756
child 1142 eb0e2ff8f032
     1.1 --- a/src/FOLP/IFOLP.thy	Wed Oct 19 09:54:38 1994 +0100
     1.2 +++ b/src/FOLP/IFOLP.thy	Fri Oct 21 09:35:24 1994 +0100
     1.3 @@ -13,7 +13,7 @@
     1.4  
     1.5  consts	
     1.6        (*** Judgements ***)
     1.7 - "@Proof"   	::   "[p,o]=>prop"	("(_ /: _)" [10,10] 5)
     1.8 + "@Proof"   	::   "[p,o]=>prop"	("(_ /: _)" [51,10] 5)
     1.9   Proof  	::   "[o,p]=>prop"
    1.10   EqProof        ::   "[p,p,o]=>prop"    ("(3_ /= _ :/ _)" [10,10,10] 5)
    1.11          
    1.12 @@ -33,7 +33,7 @@
    1.13   NORM		::	"o => o"
    1.14   norm		::	"'a => 'a"
    1.15  
    1.16 -      (*** Proof Term Formers ***)
    1.17 +      (*** Proof Term Formers: precedence must exceed 50 ***)
    1.18   tt		:: "p"
    1.19   contr		:: "p=>p"
    1.20   fst,snd	:: "p=>p"
    1.21 @@ -41,10 +41,10 @@
    1.22   split		:: "[p, [p,p]=>p] =>p"
    1.23   inl,inr	:: "p=>p"
    1.24   when		:: "[p, p=>p, p=>p]=>p"
    1.25 - lambda		:: "(p => p) => p"	(binder "lam " 20)
    1.26 + lambda		:: "(p => p) => p"	(binder "lam " 55)
    1.27   "`"		:: "[p,p]=>p"		(infixl 60)
    1.28 - alll           :: "['a=>p]=>p"         (binder "all " 15)
    1.29 - "^"            :: "[p,'a]=>p"          (infixl 50)
    1.30 + alll           :: "['a=>p]=>p"         (binder "all " 55)
    1.31 + "^"            :: "[p,'a]=>p"          (infixl 55)
    1.32   exists		:: "['a,p]=>p"		("(1[_,/_])")
    1.33   xsplit         :: "[p,['a,p]=>p]=>p"
    1.34   ideq           :: "'a=>p"