# HG changeset patch
# User clasohm
# Date 772884221 -7200
# Node ID 13ac1fd0a14dc97447629b9feaa4e514779b4d3a
# Parent  2b97bd6415b79e0a8f4d2d342232b5908a3c44b9
added parentheses made necessary by change of constrain's precedence

diff -r 2b97bd6415b7 -r 13ac1fd0a14d src/CCL/Fix.ML
--- a/src/CCL/Fix.ML	Wed Jun 29 12:01:17 1994 +0200
+++ b/src/CCL/Fix.ML	Wed Jun 29 12:03:41 1994 +0200
@@ -67,7 +67,7 @@
 by (fast_tac (set_cs addSIs ([inclI] @ (prems RL [inclD]))) 1);;
 val ball_INCL = result();
 
-goal Fix.thy "INCL(%x.a(x) = b(x)::'a::prog)";
+goal Fix.thy "INCL(%x.a(x) = (b(x)::'a::prog))";
 by (simp_tac (term_ss addsimps [eq_iff]) 1);
 by (REPEAT (resolve_tac [conj_INCL,po_INCL] 1));
 val eq_INCL = result();
diff -r 2b97bd6415b7 -r 13ac1fd0a14d src/HOLCF/Cfun2.thy
--- a/src/HOLCF/Cfun2.thy	Wed Jun 29 12:01:17 1994 +0200
+++ b/src/HOLCF/Cfun2.thy	Wed Jun 29 12:03:41 1994 +0200
@@ -19,7 +19,7 @@
 
 (* instance of << for type ['a -> 'b]  *)
 
-inst_cfun_po	"(op <<)::['a->'b,'a->'b]=>bool = less_cfun"
+inst_cfun_po	"((op <<)::['a->'b,'a->'b]=>bool) = less_cfun"
 
 (* definitions *)
 (* The least element in type 'a->'b *)
diff -r 2b97bd6415b7 -r 13ac1fd0a14d src/HOLCF/Cfun3.thy
--- a/src/HOLCF/Cfun3.thy	Wed Jun 29 12:01:17 1994 +0200
+++ b/src/HOLCF/Cfun3.thy	Wed Jun 29 12:03:41 1994 +0200
@@ -17,7 +17,7 @@
 
 rules 
 
-inst_cfun_pcpo	"UU::'a->'b = UU_cfun"
+inst_cfun_pcpo	"(UU::'a->'b) = UU_cfun"
 
 Istrictify_def	"Istrictify(f,x) == (@z.\
 \			  ( x=UU --> z = UU)\
diff -r 2b97bd6415b7 -r 13ac1fd0a14d src/HOLCF/Cprod2.thy
--- a/src/HOLCF/Cprod2.thy	Wed Jun 29 12:01:17 1994 +0200
+++ b/src/HOLCF/Cprod2.thy	Wed Jun 29 12:03:41 1994 +0200
@@ -17,7 +17,7 @@
 
 (* instance of << for type ['a * 'b]  *)
 
-inst_cprod_po	"(op <<)::['a * 'b,'a * 'b]=>bool = less_cprod"
+inst_cprod_po	"((op <<)::['a * 'b,'a * 'b]=>bool) = less_cprod"
 
 end
 
diff -r 2b97bd6415b7 -r 13ac1fd0a14d src/HOLCF/Cprod3.thy
--- a/src/HOLCF/Cprod3.thy	Wed Jun 29 12:01:17 1994 +0200
+++ b/src/HOLCF/Cprod3.thy	Wed Jun 29 12:03:41 1994 +0200
@@ -22,7 +22,7 @@
 
 rules 
 
-inst_cprod_pcpo	"UU::'a*'b = <UU,UU>"
+inst_cprod_pcpo	"(UU::'a*'b) = <UU,UU>"
 
 cpair_def	"cpair  == (LAM x y.<x,y>)"
 cfst_def	"cfst   == (LAM p.fst(p))"
diff -r 2b97bd6415b7 -r 13ac1fd0a14d src/HOLCF/Fix.ML
--- a/src/HOLCF/Fix.ML	Wed Jun 29 12:01:17 1994 +0200
+++ b/src/HOLCF/Fix.ML	Wed Jun 29 12:03:41 1994 +0200
@@ -1138,17 +1138,17 @@
 (* ------------------------------------------------------------------------- *)
 
 val flat_codom = prove_goalw Fix.thy [flat_def]
-"[|flat(y::'b);f[x::'a]=(c::'b)|] ==> f[UU::'a]=UU::'b | (!z.f[z::'a]=c)"
+"[|flat(y::'b);f[x::'a]=(c::'b)|] ==> f[UU::'a]=(UU::'b) | (!z.f[z::'a]=c)"
  (fn prems =>
 	[
 	(cut_facts_tac prems 1),
-	(res_inst_tac [("Q","f[x::'a]=UU::'b")] classical2 1),
+	(res_inst_tac [("Q","f[x::'a]=(UU::'b)")] classical2 1),
 	(rtac disjI1 1),
 	(rtac UU_I 1),
 	(res_inst_tac [("s","f[x]"),("t","UU::'b")] subst 1),
 	(atac 1),
 	(rtac (minimal RS monofun_cfun_arg) 1),
-	(res_inst_tac [("Q","f[UU::'a]=UU::'b")] classical2 1),
+	(res_inst_tac [("Q","f[UU::'a]=(UU::'b)")] classical2 1),
 	(etac disjI1 1),
 	(rtac disjI2 1),
 	(rtac allI 1),
diff -r 2b97bd6415b7 -r 13ac1fd0a14d src/HOLCF/Fix.thy
--- a/src/HOLCF/Fix.thy	Wed Jun 29 12:01:17 1994 +0200
+++ b/src/HOLCF/Fix.thy	Wed Jun 29 12:03:41 1994 +0200
@@ -36,7 +36,7 @@
 \                        !Y. is_chain(Y::nat=>'a) --> (? n.max_in_chain(n,Y))"
 
 flat_def          "flat(x::'a) ==\
-\                        ! x y. x::'a << y --> (x = UU) | (x=y)"
+\                        ! x y. (x::'a) << y --> (x = UU) | (x=y)"
 
 end
 
diff -r 2b97bd6415b7 -r 13ac1fd0a14d src/HOLCF/Fun2.thy
--- a/src/HOLCF/Fun2.thy	Wed Jun 29 12:01:17 1994 +0200
+++ b/src/HOLCF/Fun2.thy	Wed Jun 29 12:03:41 1994 +0200
@@ -22,7 +22,7 @@
 
 (* instance of << for type ['a::term => 'b::po]  *)
 
-inst_fun_po	"(op <<)::['a=>'b::po,'a=>'b::po ]=>bool = less_fun"
+inst_fun_po	"((op <<)::['a=>'b::po,'a=>'b::po ]=>bool) = less_fun"
 
 (* definitions *)
 (* The least element in type 'a::term => 'b::pcpo *)
diff -r 2b97bd6415b7 -r 13ac1fd0a14d src/HOLCF/Fun3.thy
--- a/src/HOLCF/Fun3.thy	Wed Jun 29 12:01:17 1994 +0200
+++ b/src/HOLCF/Fun3.thy	Wed Jun 29 12:03:41 1994 +0200
@@ -15,7 +15,7 @@
 
 rules 
 
-inst_fun_pcpo	"UU::'a=>'b::pcpo = UU_fun"
+inst_fun_pcpo	"(UU::'a=>'b::pcpo) = UU_fun"
 
 end
 
diff -r 2b97bd6415b7 -r 13ac1fd0a14d src/HOLCF/Lift2.thy
--- a/src/HOLCF/Lift2.thy	Wed Jun 29 12:01:17 1994 +0200
+++ b/src/HOLCF/Lift2.thy	Wed Jun 29 12:03:41 1994 +0200
@@ -17,7 +17,7 @@
 
 (* instance of << for type ('a)u  *)
 
-inst_lift_po	"(op <<)::[('a)u,('a)u]=>bool = less_lift"
+inst_lift_po	"((op <<)::[('a)u,('a)u]=>bool) = less_lift"
 
 end
 
diff -r 2b97bd6415b7 -r 13ac1fd0a14d src/HOLCF/Lift3.thy
--- a/src/HOLCF/Lift3.thy	Wed Jun 29 12:01:17 1994 +0200
+++ b/src/HOLCF/Lift3.thy	Wed Jun 29 12:03:41 1994 +0200
@@ -18,7 +18,7 @@
 
 rules 
 
-inst_lift_pcpo	"UU::('a)u = UU_lift"
+inst_lift_pcpo	"(UU::('a)u) = UU_lift"
 
 up_def		"up     == (LAM x.Iup(x))"
 lift_def	"lift   == (LAM f p.Ilift(f)(p))"
diff -r 2b97bd6415b7 -r 13ac1fd0a14d src/HOLCF/Pcpo.ML
--- a/src/HOLCF/Pcpo.ML	Wed Jun 29 12:01:17 1994 +0200
+++ b/src/HOLCF/Pcpo.ML	Wed Jun 29 12:03:41 1994 +0200
@@ -13,7 +13,7 @@
 (* ------------------------------------------------------------------------ *)
 
 val thelubE = prove_goal  Pcpo.thy 
-	"[| is_chain(S);lub(range(S)) = l::'a::pcpo|] ==> range(S) <<| l "
+	"[| is_chain(S);lub(range(S)) = (l::'a::pcpo)|] ==> range(S) <<| l "
 (fn prems =>
 	[
 	(cut_facts_tac prems 1), 
@@ -256,7 +256,7 @@
 (* uniqueness in void                                                       *)
 (* ------------------------------------------------------------------------ *)
 
-val unique_void2 = prove_goal Pcpo.thy "x::void=UU"
+val unique_void2 = prove_goal Pcpo.thy "(x::void)=UU"
  (fn prems =>
 	[
 	(rtac (inst_void_pcpo RS ssubst) 1),
diff -r 2b97bd6415b7 -r 13ac1fd0a14d src/HOLCF/Pcpo.thy
--- a/src/HOLCF/Pcpo.thy	Wed Jun 29 12:01:17 1994 +0200
+++ b/src/HOLCF/Pcpo.thy	Wed Jun 29 12:03:41 1994 +0200
@@ -28,12 +28,12 @@
 
 minimal		"UU << x"			(* witness is minimal_void *)
 
-cpo		"is_chain(S) ==> ? x. range(S) <<| x::('a::pcpo)" 
+cpo		"is_chain(S) ==> ? x. range(S) <<| (x::('a::pcpo))" 
 						(* witness is cpo_void     *)
 						(* needs explicit type     *)
 
 (* instance of UU for the prototype void *)
 
-inst_void_pcpo	"UU::void = UU_void"
+inst_void_pcpo	"(UU::void) = UU_void"
 
 end 
diff -r 2b97bd6415b7 -r 13ac1fd0a14d src/HOLCF/Porder.ML
--- a/src/HOLCF/Porder.ML	Wed Jun 29 12:01:17 1994 +0200
+++ b/src/HOLCF/Porder.ML	Wed Jun 29 12:03:41 1994 +0200
@@ -77,7 +77,7 @@
 (* ------------------------------------------------------------------------ *)
 
 val nat_less_cases = prove_goal Porder.thy 
-	"[| m::nat < n ==> P(n,m); m=n ==> P(n,m);n < m ==> P(n,m)|]==>P(n,m)"
+	"[| (m::nat) < n ==> P(n,m); m=n ==> P(n,m);n < m ==> P(n,m)|]==>P(n,m)"
 ( fn prems =>
 	[
 	(res_inst_tac [("m1","n"),("n1","m")] (less_linear RS disjE) 1),
@@ -236,7 +236,7 @@
 (* a technical argument about << on void                                    *)
 (* ------------------------------------------------------------------------ *)
 
-val less_void = prove_goal Porder.thy "(u1::void << u2) = (u1 = u2)"
+val less_void = prove_goal Porder.thy "((u1::void) << u2) = (u1 = u2)"
 (fn prems =>
 	[
 	(rtac (inst_void_po RS ssubst) 1),
@@ -289,7 +289,7 @@
 (* ------------------------------------------------------------------------ *)
 
 val cpo_void = prove_goal Porder.thy
-	"is_chain(S::nat=>void) ==> ? x. range(S) <<| x "
+	"is_chain((S::nat=>void)) ==> ? x. range(S) <<| x "
 (fn prems =>
 	[
 	(cut_facts_tac prems 1),
diff -r 2b97bd6415b7 -r 13ac1fd0a14d src/HOLCF/Porder0.thy
--- a/src/HOLCF/Porder0.thy	Wed Jun 29 12:01:17 1994 +0200
+++ b/src/HOLCF/Porder0.thy	Wed Jun 29 12:03:41 1994 +0200
@@ -37,6 +37,6 @@
 
 (* instance of << for the prototype void *)
 
-inst_void_po	"(op <<)::[void,void]=>bool = less_void"
+inst_void_po	"((op <<)::[void,void]=>bool) = less_void"
 
 end 
diff -r 2b97bd6415b7 -r 13ac1fd0a14d src/HOLCF/Sprod2.thy
--- a/src/HOLCF/Sprod2.thy	Wed Jun 29 12:01:17 1994 +0200
+++ b/src/HOLCF/Sprod2.thy	Wed Jun 29 12:03:41 1994 +0200
@@ -16,7 +16,7 @@
 
 (* instance of << for type ['a ** 'b]  *)
 
-inst_sprod_po	"(op <<)::['a ** 'b,'a ** 'b]=>bool = less_sprod"
+inst_sprod_po	"((op <<)::['a ** 'b,'a ** 'b]=>bool) = less_sprod"
 
 end
 
diff -r 2b97bd6415b7 -r 13ac1fd0a14d src/HOLCF/Sprod3.thy
--- a/src/HOLCF/Sprod3.thy	Wed Jun 29 12:01:17 1994 +0200
+++ b/src/HOLCF/Sprod3.thy	Wed Jun 29 12:03:41 1994 +0200
@@ -20,7 +20,7 @@
 
 rules 
 
-inst_sprod_pcpo	"UU::'a**'b = Ispair(UU,UU)"
+inst_sprod_pcpo	"(UU::'a**'b) = Ispair(UU,UU)"
 spair_def	"spair  == (LAM x y.Ispair(x,y))"
 sfst_def	"sfst   == (LAM p.Isfst(p))"
 ssnd_def	"ssnd   == (LAM p.Issnd(p))"	
diff -r 2b97bd6415b7 -r 13ac1fd0a14d src/HOLCF/Ssum2.thy
--- a/src/HOLCF/Ssum2.thy	Wed Jun 29 12:01:17 1994 +0200
+++ b/src/HOLCF/Ssum2.thy	Wed Jun 29 12:03:41 1994 +0200
@@ -15,7 +15,7 @@
 
 (* instance of << for type ['a ++ 'b]  *)
 
-inst_ssum_po	"(op <<)::['a ++ 'b,'a ++ 'b]=>bool = less_ssum"
+inst_ssum_po	"((op <<)::['a ++ 'b,'a ++ 'b]=>bool) = less_ssum"
 
 end
 
diff -r 2b97bd6415b7 -r 13ac1fd0a14d src/HOLCF/Ssum3.thy
--- a/src/HOLCF/Ssum3.thy	Wed Jun 29 12:01:17 1994 +0200
+++ b/src/HOLCF/Ssum3.thy	Wed Jun 29 12:03:41 1994 +0200
@@ -17,7 +17,7 @@
 
 rules 
 
-inst_ssum_pcpo	"UU::'a++'b = Isinl(UU)"
+inst_ssum_pcpo	"(UU::'a++'b) = Isinl(UU)"
 
 sinl_def	"sinl   == (LAM x.Isinl(x))"
 sinr_def	"sinr   == (LAM x.Isinr(x))"
diff -r 2b97bd6415b7 -r 13ac1fd0a14d src/HOLCF/ex/Hoare.ML
--- a/src/HOLCF/ex/Hoare.ML	Wed Jun 29 12:01:17 1994 +0200
+++ b/src/HOLCF/ex/Hoare.ML	Wed Jun 29 12:03:41 1994 +0200
@@ -90,7 +90,7 @@
 	]);
 
 val hoare_lemma28 = prove_goal HOLCF.thy 
-"b1[y::'a]=UU::tr ==> b1[UU] = UU"
+"b1[y::'a]=(UU::tr) ==> b1[UU] = UU"
  (fn prems =>
 	[
 	(cut_facts_tac prems 1),
diff -r 2b97bd6415b7 -r 13ac1fd0a14d src/LCF/LCF.ML
--- a/src/LCF/LCF.ML	Wed Jun 29 12:01:17 1994 +0200
+++ b/src/LCF/LCF.ML	Wed Jun 29 12:03:41 1994 +0200
@@ -65,7 +65,7 @@
 		      REPEAT(rstac(conjI::prems)1)]);
 
 val ext = prove_goal thy
-	"(!!x::'a::cpo. f(x)=g(x)::'b::cpo) ==> (%x.f(x))=(%x.g(x))"
+	"(!!x::'a::cpo. f(x)=(g(x)::'b::cpo)) ==> (%x.f(x))=(%x.g(x))"
 	(fn [prem] => [REPEAT(rstac[less_anti_sym, less_ext, allI,
 				    prem RS eq_imp_less1,
 				    prem RS eq_imp_less2]1)]);
diff -r 2b97bd6415b7 -r 13ac1fd0a14d src/LCF/fix.ML
--- a/src/LCF/fix.ML	Wed Jun 29 12:01:17 1994 +0200
+++ b/src/LCF/fix.ML	Wed Jun 29 12:03:41 1994 +0200
@@ -14,7 +14,7 @@
 structure Fix:FIX =
 struct
 
-val adm_eq = prove_goal LCF.thy "adm(%x.t(x)=u(x)::'a::cpo)"
+val adm_eq = prove_goal LCF.thy "adm(%x.t(x)=(u(x)::'a::cpo))"
 	(fn _ => [rewrite_goals_tac [eq_def],
 		  REPEAT(rstac[adm_conj,adm_less]1)]);
 
diff -r 2b97bd6415b7 -r 13ac1fd0a14d src/LCF/pair.ML
--- a/src/LCF/pair.ML	Wed Jun 29 12:01:17 1994 +0200
+++ b/src/LCF/pair.ML	Wed Jun 29 12:03:41 1994 +0200
@@ -8,7 +8,7 @@
 val qpair = read_instantiate [("z","q::'a*'b")] surj_pairing;
 in
 val PROD_less = prove_goal LCF.thy
-	"p::'a*'b << q <-> FST(p) << FST(q) & SND(p) << SND(q)"
+	"(p::'a*'b) << q <-> FST(p) << FST(q) & SND(p) << SND(q)"
 	(fn _ => [EVERY1[rtac iffI,
 		  rtac conjI, etac less_ap_term, etac less_ap_term,
 		  rtac (ppair RS subst), rtac (qpair RS subst),