# HG changeset patch
# User lcp
# Date 782728524 -3600
# Node ID e27c9ec2b48bd3e42939a48763b01473e493553e
# Parent  fb7345cccddc4628dcdad42d6208ee84563b4450
FOLP/IFOLP.thy: tightening precedences to eliminate syntactic ambiguities.
Now proof objects have high precedences.  Eliminates ambiguity in a=b:P
being parsed as (a=b):P.

diff -r fb7345cccddc -r e27c9ec2b48b src/FOLP/IFOLP.thy
--- a/src/FOLP/IFOLP.thy	Wed Oct 19 09:54:38 1994 +0100
+++ b/src/FOLP/IFOLP.thy	Fri Oct 21 09:35:24 1994 +0100
@@ -13,7 +13,7 @@
 
 consts	
       (*** Judgements ***)
- "@Proof"   	::   "[p,o]=>prop"	("(_ /: _)" [10,10] 5)
+ "@Proof"   	::   "[p,o]=>prop"	("(_ /: _)" [51,10] 5)
  Proof  	::   "[o,p]=>prop"
  EqProof        ::   "[p,p,o]=>prop"    ("(3_ /= _ :/ _)" [10,10,10] 5)
         
@@ -33,7 +33,7 @@
  NORM		::	"o => o"
  norm		::	"'a => 'a"
 
-      (*** Proof Term Formers ***)
+      (*** Proof Term Formers: precedence must exceed 50 ***)
  tt		:: "p"
  contr		:: "p=>p"
  fst,snd	:: "p=>p"
@@ -41,10 +41,10 @@
  split		:: "[p, [p,p]=>p] =>p"
  inl,inr	:: "p=>p"
  when		:: "[p, p=>p, p=>p]=>p"
- lambda		:: "(p => p) => p"	(binder "lam " 20)
+ lambda		:: "(p => p) => p"	(binder "lam " 55)
  "`"		:: "[p,p]=>p"		(infixl 60)
- alll           :: "['a=>p]=>p"         (binder "all " 15)
- "^"            :: "[p,'a]=>p"          (infixl 50)
+ alll           :: "['a=>p]=>p"         (binder "all " 55)
+ "^"            :: "[p,'a]=>p"          (infixl 55)
  exists		:: "['a,p]=>p"		("(1[_,/_])")
  xsplit         :: "[p,['a,p]=>p]=>p"
  ideq           :: "'a=>p"