--- 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();
--- 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 *)
--- 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)\
--- 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
--- 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))"
--- 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),
--- 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
--- 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 *)
--- 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
--- 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
--- 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))"
--- 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),
--- 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
--- 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),
--- 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
--- 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
--- 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))"
--- 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
--- 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))"
--- 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),
--- 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)]);
--- 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)]);
--- 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),