Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
FOLP/IFOLP.thy: tightening precedences to eliminate syntactic ambiguities.
authorlcp
Fri, 21 Oct 1994 09:35:24 +0100
changeset 648 e27c9ec2b48b
parent 647 fb7345cccddc
child 649 237fce674bfb
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.
src/FOLP/IFOLP.thy file | annotate | diff | comparison | revisions 
--- 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"
isabelle