# HG changeset patch
# User clasohm
# Date 772884244 -7200
# Node ID 5c7a69cef18bc95f0231694c9d455dc39266a554
# Parent  5f462dfaf130c5f6bd3abe814d22a04cee6fb8c8
added parentheses made necessary by change of constrain's precedence

diff -r 5f462dfaf130 -r 5c7a69cef18b Arith.ML
--- a/Arith.ML	Fri Jun 24 15:11:39 1994 +0200
+++ b/Arith.ML	Wed Jun 29 12:04:04 1994 +0200
@@ -53,14 +53,14 @@
 val arith_ss = arith_ss addsimps [add_0_right,add_Suc_right];
 
 (*Associative law for addition*)
-val add_assoc = prove_goal Arith.thy "(m + n) + k = m + (n + k)::nat"
+val add_assoc = prove_goal Arith.thy "(m + n) + k = m + ((n + k)::nat)"
  (fn _ => [nat_ind_tac "m" 1, ALLGOALS(asm_simp_tac arith_ss)]);
 
 (*Commutative law for addition*)  
-val add_commute = prove_goal Arith.thy "m + n = n + m::nat"
+val add_commute = prove_goal Arith.thy "m + n = n + (m::nat)"
  (fn _ =>  [nat_ind_tac "m" 1, ALLGOALS(asm_simp_tac arith_ss)]);
 
-val add_left_commute = prove_goal Arith.thy "x+(y+z)=y+(x+z)::nat"
+val add_left_commute = prove_goal Arith.thy "x+(y+z)=y+((x+z)::nat)"
  (fn _ => [rtac (add_commute RS trans) 1, rtac (add_assoc RS trans) 1,
            rtac (add_commute RS arg_cong) 1]);
 
@@ -82,25 +82,25 @@
 val arith_ss = arith_ss addsimps [mult_0_right,mult_Suc_right];
 
 (*Commutative law for multiplication*)
-val mult_commute = prove_goal Arith.thy "m * n = n * m::nat"
+val mult_commute = prove_goal Arith.thy "m * n = n * (m::nat)"
  (fn _ => [nat_ind_tac "m" 1, ALLGOALS (asm_simp_tac arith_ss)]);
 
 (*addition distributes over multiplication*)
-val add_mult_distrib = prove_goal Arith.thy "(m + n)*k = (m*k) + (n*k)::nat"
+val add_mult_distrib = prove_goal Arith.thy "(m + n)*k = (m*k) + ((n*k)::nat)"
  (fn _ => [nat_ind_tac "m" 1,
            ALLGOALS(asm_simp_tac (arith_ss addsimps add_ac))]);
 
-val add_mult_distrib2 = prove_goal Arith.thy "k*(m + n) = (k*m) + (k*n)::nat"
+val add_mult_distrib2 = prove_goal Arith.thy "k*(m + n) = (k*m) + ((k*n)::nat)"
  (fn _ => [nat_ind_tac "m" 1,
            ALLGOALS(asm_simp_tac (arith_ss addsimps add_ac))]);
 
 val arith_ss = arith_ss addsimps [add_mult_distrib,add_mult_distrib2];
 
 (*Associative law for multiplication*)
-val mult_assoc = prove_goal Arith.thy "(m * n) * k = m * (n * k)::nat"
+val mult_assoc = prove_goal Arith.thy "(m * n) * k = m * ((n * k)::nat)"
   (fn _ => [nat_ind_tac "m" 1, ALLGOALS(asm_simp_tac arith_ss)]);
 
-val mult_left_commute = prove_goal Arith.thy "x*(y*z) = y*(x*z)::nat"
+val mult_left_commute = prove_goal Arith.thy "x*(y*z) = y*((x*z)::nat)"
  (fn _ => [rtac trans 1, rtac mult_commute 1, rtac trans 1,
            rtac mult_assoc 1, rtac (mult_commute RS arg_cong) 1]);
 
@@ -112,7 +112,7 @@
  (fn _ => [nat_ind_tac "m" 1, ALLGOALS(asm_simp_tac arith_ss)]);
 
 (*Addition is the inverse of subtraction: if n<=m then n+(m-n) = m. *)
-val [prem] = goal Arith.thy "[| ~ m<n |] ==> n+(m-n) = m::nat";
+val [prem] = goal Arith.thy "[| ~ m<n |] ==> n+(m-n) = (m::nat)";
 by (rtac (prem RS rev_mp) 1);
 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
 by (ALLGOALS(asm_simp_tac arith_ss));
@@ -223,14 +223,14 @@
 
 (**** Additional theorems about "less than" ****)
 
-goal Arith.thy "n <= (m + n)::nat";
+goal Arith.thy "n <= ((m + n)::nat)";
 by (nat_ind_tac "m" 1);
 by (ALLGOALS(simp_tac arith_ss));
 by (etac le_trans 1);
 by (rtac (lessI RS less_imp_le) 1);
 val le_add2 = result();
 
-goal Arith.thy "n <= (n + m)::nat";
+goal Arith.thy "n <= ((n + m)::nat)";
 by (simp_tac (arith_ss addsimps add_ac) 1);
 by (rtac le_add2 1);
 val le_add1 = result();
@@ -238,7 +238,7 @@
 val less_add_Suc1 = standard (lessI RS (le_add1 RS le_less_trans));
 val less_add_Suc2 = standard (lessI RS (le_add2 RS le_less_trans));
 
-goal Arith.thy "m+k<=n --> m<=n::nat";
+goal Arith.thy "m+k<=n --> m<=(n::nat)";
 by (nat_ind_tac "k" 1);
 by (ALLGOALS (asm_simp_tac arith_ss));
 by (fast_tac (HOL_cs addDs [Suc_leD]) 1);
diff -r 5f462dfaf130 -r 5c7a69cef18b HOL.ML
--- a/HOL.ML	Fri Jun 24 15:11:39 1994 +0200
+++ b/HOL.ML	Wed Jun 29 12:04:04 1994 +0200
@@ -103,7 +103,7 @@
  (fn [prem] => [rtac (prem RS subst) 1, rtac refl 1]);
 
 val cong = prove_goal HOL.thy
-   "[| f = g; x::'a = y |] ==> f(x) = g(y)"
+   "[| f = g; (x::'a) = y |] ==> f(x) = g(y)"
  (fn [prem1,prem2] =>
    [rtac (prem1 RS subst) 1, rtac (prem2 RS subst) 1, rtac refl 1]);
 
diff -r 5f462dfaf130 -r 5c7a69cef18b HOL.thy
--- a/HOL.thy	Fri Jun 24 15:11:39 1994 +0200
+++ b/HOL.thy	Wed Jun 29 12:04:04 1994 +0200
@@ -93,9 +93,9 @@
 
   (* Basic Rules *)
 
-  refl          "t = t::'a"
+  refl          "t = (t::'a)"
   subst         "[| s = t; P(s) |] ==> P(t::'a)"
-  ext           "(!!x::'a. f(x)::'b = g(x)) ==> (%x.f(x)) = (%x.g(x))"
+  ext           "(!!x::'a. (f(x)::'b) = g(x)) ==> (%x.f(x)) = (%x.g(x))"
   selectI       "P(x::'a) ==> P(@x.P(x))"
 
   impI          "(P ==> Q) ==> P-->Q"
diff -r 5f462dfaf130 -r 5c7a69cef18b LList.ML
--- a/LList.ML	Fri Jun 24 15:11:39 1994 +0200
+++ b/LList.ML	Wed Jun 29 12:04:04 1994 +0200
@@ -715,7 +715,7 @@
     "[| f(LNil)=g(LNil);						\
 \       !!x l. <f(LCons(x,l)),g(LCons(x,l))> :				\
 \              llistD_Fun(range(%u. <f(u),g(u)>) Un range(%v. <v,v>))	\
-\    |]	==> f(l) = g(l :: 'a llist) :: 'b llist";
+\    |]	==> f(l) = (g(l :: 'a llist) :: 'b llist)";
 by (res_inst_tac [("r", "range(%u. <f(u),g(u)>)")] llist_equalityI 1);
 by (rtac rangeI 1);
 by (rtac subsetI 1);
diff -r 5f462dfaf130 -r 5c7a69cef18b Nat.ML
--- a/Nat.ML	Fri Jun 24 15:11:39 1994 +0200
+++ b/Nat.ML	Wed Jun 29 12:04:04 1994 +0200
@@ -196,7 +196,7 @@
 
 (** Introduction properties **)
 
-val prems = goalw Nat.thy [less_def] "[| i<j;  j<k |] ==> i<k::nat";
+val prems = goalw Nat.thy [less_def] "[| i<j;  j<k |] ==> i<(k::nat)";
 by (rtac (trans_trancl RS transD) 1);
 by (resolve_tac prems 1);
 by (resolve_tac prems 1);
@@ -218,14 +218,14 @@
 
 (** Elimination properties **)
 
-val prems = goalw Nat.thy [less_def] "n<m ==> ~ m<n::nat";
+val prems = goalw Nat.thy [less_def] "n<m ==> ~ m<(n::nat)";
 by(fast_tac (HOL_cs addIs ([wf_pred_nat, wf_trancl RS wf_asym]@prems))1);
 val less_not_sym = result();
 
 (* [| n<m; m<n |] ==> R *)
 val less_asym = standard (less_not_sym RS notE);
 
-goalw Nat.thy [less_def] "~ n<n::nat";
+goalw Nat.thy [less_def] "~ n<(n::nat)";
 by (rtac notI 1);
 by (etac (wf_pred_nat RS wf_trancl RS wf_anti_refl) 1);
 val less_not_refl = result();
@@ -233,7 +233,7 @@
 (* n<n ==> R *)
 val less_anti_refl = standard (less_not_refl RS notE);
 
-goal Nat.thy "!!m. n<m ==> m ~= n::nat";
+goal Nat.thy "!!m. n<m ==> m ~= (n::nat)";
 by(fast_tac (HOL_cs addEs [less_anti_refl]) 1);
 val less_not_refl2 = result();
 
@@ -318,7 +318,7 @@
 val not_Suc_n_less_n = result();
 
 (*"Less than" is a linear ordering*)
-goal Nat.thy "m<n | m=n | n<m::nat";
+goal Nat.thy "m<n | m=n | n<(m::nat)";
 by (nat_ind_tac "m" 1);
 by (nat_ind_tac "n" 1);
 by (rtac (refl RS disjI1 RS disjI2) 1);
@@ -364,17 +364,17 @@
   "m=n ==> nat_rec(m,a,f) = nat_rec(n,a,f)"
   (fn [prem] => [rtac (prem RS arg_cong) 1]);
 
-val prems = goalw Nat.thy [le_def] "~(n<m) ==> m<=n::nat";
+val prems = goalw Nat.thy [le_def] "~(n<m) ==> m<=(n::nat)";
 by (resolve_tac prems 1);
 val leI = result();
 
-val prems = goalw Nat.thy [le_def] "m<=n ==> ~(n<m::nat)";
+val prems = goalw Nat.thy [le_def] "m<=n ==> ~(n<(m::nat))";
 by (resolve_tac prems 1);
 val leD = result();
 
 val leE = make_elim leD;
 
-goalw Nat.thy [le_def] "!!m. ~ m <= n ==> n<m::nat";
+goalw Nat.thy [le_def] "!!m. ~ m <= n ==> n<(m::nat)";
 by (fast_tac HOL_cs 1);
 val not_leE = result();
 
@@ -388,40 +388,40 @@
 by(fast_tac HOL_cs 1);
 val Suc_leD = result();
 
-goalw Nat.thy [le_def] "!!m. m < n ==> m <= n::nat";
+goalw Nat.thy [le_def] "!!m. m < n ==> m <= (n::nat)";
 by (fast_tac (HOL_cs addEs [less_asym]) 1);
 val less_imp_le = result();
 
-goalw Nat.thy [le_def] "!!m. m <= n ==> m < n | m=n::nat";
+goalw Nat.thy [le_def] "!!m. m <= n ==> m < n | m=(n::nat)";
 by (cut_facts_tac [less_linear] 1);
 by (fast_tac (HOL_cs addEs [less_anti_refl,less_asym]) 1);
 val le_imp_less_or_eq = result();
 
-goalw Nat.thy [le_def] "!!m. m<n | m=n ==> m <= n::nat";
+goalw Nat.thy [le_def] "!!m. m<n | m=n ==> m <=(n::nat)";
 by (cut_facts_tac [less_linear] 1);
 by (fast_tac (HOL_cs addEs [less_anti_refl,less_asym]) 1);
 by (flexflex_tac);
 val less_or_eq_imp_le = result();
 
-goal Nat.thy "(x <= y::nat) = (x < y | x=y)";
+goal Nat.thy "(x <= (y::nat)) = (x < y | x=y)";
 by (REPEAT(ares_tac [iffI,less_or_eq_imp_le,le_imp_less_or_eq] 1));
 val le_eq_less_or_eq = result();
 
-goal Nat.thy "n <= n::nat";
+goal Nat.thy "n <= (n::nat)";
 by(simp_tac (HOL_ss addsimps [le_eq_less_or_eq]) 1);
 val le_refl = result();
 
-val prems = goal Nat.thy "!!i. [| i <= j; j < k |] ==> i < k::nat";
+val prems = goal Nat.thy "!!i. [| i <= j; j < k |] ==> i < (k::nat)";
 by (dtac le_imp_less_or_eq 1);
 by (fast_tac (HOL_cs addIs [less_trans]) 1);
 val le_less_trans = result();
 
-goal Nat.thy "!!i. [| i <= j; j <= k |] ==> i <= k::nat";
+goal Nat.thy "!!i. [| i <= j; j <= k |] ==> i <= (k::nat)";
 by (EVERY1[dtac le_imp_less_or_eq, dtac le_imp_less_or_eq,
           rtac less_or_eq_imp_le, fast_tac (HOL_cs addIs [less_trans])]);
 val le_trans = result();
 
-val prems = goal Nat.thy "!!m. [| m <= n; n <= m |] ==> m = n::nat";
+val prems = goal Nat.thy "!!m. [| m <= n; n <= m |] ==> m = (n::nat)";
 by (EVERY1[dtac le_imp_less_or_eq, dtac le_imp_less_or_eq,
           fast_tac (HOL_cs addEs [less_anti_refl,less_asym])]);
 val le_anti_sym = result();
diff -r 5f462dfaf130 -r 5c7a69cef18b Nat.thy
--- a/Nat.thy	Fri Jun 24 15:11:39 1994 +0200
+++ b/Nat.thy	Wed Jun 29 12:04:04 1994 +0200
@@ -49,7 +49,7 @@
 
   less_def "m<n == <m,n>:trancl(pred_nat)"
 
-  le_def   "m<=n::nat == ~(n<m)"
+  le_def   "m<=(n::nat) == ~(n<m)"
 
   nat_rec_def	"nat_rec(n,c,d) == wfrec(pred_nat, n,   \
 \                        %l g. nat_case(l, c, %m. d(m,g(m))))"
diff -r 5f462dfaf130 -r 5c7a69cef18b Set.ML
--- a/Set.ML	Fri Jun 24 15:11:39 1994 +0200
+++ b/Set.ML	Wed Jun 29 12:04:04 1994 +0200
@@ -117,10 +117,10 @@
 (*Takes assumptions A<=B; c:A and creates the assumption c:B *)
 fun set_mp_tac i = etac subsetCE i  THEN  mp_tac i;
 
-val subset_refl = prove_goal Set.thy "A <= A::'a set"
+val subset_refl = prove_goal Set.thy "A <= (A::'a set)"
  (fn _=> [ (REPEAT (ares_tac [subsetI] 1)) ]);
 
-val prems = goal Set.thy "[| A<=B;  B<=C |] ==> A<=C::'a set";
+val prems = goal Set.thy "[| A<=B;  B<=C |] ==> A<=(C::'a set)";
 by (cut_facts_tac prems 1);
 by (REPEAT (ares_tac [subsetI] 1 ORELSE set_mp_tac 1));
 val subset_trans = result();
@@ -129,25 +129,25 @@
 (*** Equality ***)
 
 (*Anti-symmetry of the subset relation*)
-val prems = goal Set.thy "[| A <= B;  B <= A |] ==> A = B::'a set";
+val prems = goal Set.thy "[| A <= B;  B <= A |] ==> A = (B::'a set)";
 by (rtac (iffI RS set_ext) 1);
 by (REPEAT (ares_tac (prems RL [subsetD]) 1));
 val subset_antisym = result();
 val equalityI = subset_antisym;
 
 (* Equality rules from ZF set theory -- are they appropriate here? *)
-val prems = goal Set.thy "A = B ==> A<=B::'a set";
+val prems = goal Set.thy "A = B ==> A<=(B::'a set)";
 by (resolve_tac (prems RL [subst]) 1);
 by (rtac subset_refl 1);
 val equalityD1 = result();
 
-val prems = goal Set.thy "A = B ==> B<=A::'a set";
+val prems = goal Set.thy "A = B ==> B<=(A::'a set)";
 by (resolve_tac (prems RL [subst]) 1);
 by (rtac subset_refl 1);
 val equalityD2 = result();
 
 val prems = goal Set.thy
-    "[| A = B;  [| A<=B; B<=A::'a set |] ==> P |]  ==>  P";
+    "[| A = B;  [| A<=B; B<=(A::'a set) |] ==> P |]  ==>  P";
 by (resolve_tac prems 1);
 by (REPEAT (resolve_tac (prems RL [equalityD1,equalityD2]) 1));
 val equalityE = result();
diff -r 5f462dfaf130 -r 5c7a69cef18b Subst/Setplus.ML
--- a/Subst/Setplus.ML	Fri Jun 24 15:11:39 1994 +0200
+++ b/Subst/Setplus.ML	Wed Jun 29 12:04:04 1994 +0200
@@ -20,7 +20,7 @@
 by (rtac refl 1);
 val ssubset_iff = result();
 
-goal Setplus.thy "(A::'a set <= B) = ((A < B) | (A=B))";
+goal Setplus.thy "((A::'a set) <= B) = ((A < B) | (A=B))";
 by (simp_tac (set_ss addsimps [ssubset_iff]) 1);
 by (fast_tac set_cs 1);
 val subseteq_iff_subset_eq = result();
diff -r 5f462dfaf130 -r 5c7a69cef18b Trancl.ML
--- a/Trancl.ML	Fri Jun 24 15:11:39 1994 +0200
+++ b/Trancl.ML	Wed Jun 29 12:04:04 1994 +0200
@@ -151,7 +151,7 @@
     "[| <a::'a,b> : r^*;  (a = b) ==> P; 	\
 \	!!y.[| <a,y> : r^*; <y,b> : r |] ==> P 	\
 \    |] ==> P";
-by (subgoal_tac "a::'a = b  | (? y. <a,y> : r^* & <y,b> : r)" 1);
+by (subgoal_tac "(a::'a) = b  | (? y. <a,y> : r^* & <y,b> : r)" 1);
 by (rtac (major RS rtrancl_induct) 2);
 by (fast_tac (set_cs addIs prems) 2);
 by (fast_tac (set_cs addIs prems) 2);
diff -r 5f462dfaf130 -r 5c7a69cef18b equalities.ML
--- a/equalities.ML	Fri Jun 24 15:11:39 1994 +0200
+++ b/equalities.ML	Wed Jun 29 12:04:04 1994 +0200
@@ -307,7 +307,7 @@
 by (fast_tac eq_cs 1);
 val Diff_partition = result();
 
-goal Set.thy "!!A. [| A<=B; B<= C |] ==> (B - (C - A)) = A :: 'a set";
+goal Set.thy "!!A. [| A<=B; B<= C |] ==> (B - (C - A)) = (A :: 'a set)";
 by (fast_tac eq_cs 1);
 val double_diff = result();
 
diff -r 5f462dfaf130 -r 5c7a69cef18b ex/cla.ML
--- a/ex/cla.ML	Fri Jun 24 15:11:39 1994 +0200
+++ b/ex/cla.ML	Wed Jun 29 12:04:04 1994 +0200
@@ -336,8 +336,8 @@
 
 writeln"Problem 43  NOT PROVED AUTOMATICALLY";
 goal HOL.thy
-    "(! x::'a. ! y::'a. q(x,y) = (! z. p(z,x) = p(z,y)::bool))	\
-\ --> (! x. (! y. q(x,y) = q(y,x)::bool))";
+    "(! x::'a. ! y::'a. q(x,y) = (! z. p(z,x) = (p(z,y)::bool)))	\
+\ --> (! x. (! y. q(x,y) = (q(y,x)::bool)))";
 
 
 writeln"Problem 44";
diff -r 5f462dfaf130 -r 5c7a69cef18b ex/mesontest.ML
--- a/ex/mesontest.ML	Fri Jun 24 15:11:39 1994 +0200
+++ b/ex/mesontest.ML	Wed Jun 29 12:04:04 1994 +0200
@@ -75,8 +75,8 @@
 
 
 writeln"Problem 43  NOW PROVED AUTOMATICALLY!!";
-goal HOL.thy "(! x. ! y. q(x,y) = (! z. p(z,x) = p(z,y)::bool))	\
-\         --> (! x. (! y. q(x,y) = q(y,x)::bool))";
+goal HOL.thy "(! x. ! y. q(x,y) = (! z. p(z,x) = (p(z,y)::bool)))	\
+\         --> (! x. (! y. q(x,y) = (q(y,x)::bool)))";
 by (rtac ccontr 1);
 val [prem43] = gethyps 1;
 val nnf43 = make_nnf prem43;
@@ -161,7 +161,7 @@
 result();
 
 (*11.  Proved in each direction (incorrectly, says Pelletier!!)  *)
-goal HOL.thy "P=P::bool";
+goal HOL.thy "P=(P::bool)";
 by (safe_meson_tac 1);
 result();
 
@@ -404,8 +404,8 @@
 result();
 
 writeln"Problem 43  NOW PROVED AUTOMATICALLY!!";
-goal HOL.thy "(! x. ! y. q(x,y) = (! z. p(z,x) = p(z,y)::bool))	\
-\         --> (! x. (! y. q(x,y) = q(y,x)::bool))";
+goal HOL.thy "(! x. ! y. q(x,y) = (! z. p(z,x) = (p(z,y)::bool)))	\
+\         --> (! x. (! y. q(x,y) = (q(y,x)::bool)))";
 by (safe_meson_tac 1);
 result();
 
diff -r 5f462dfaf130 -r 5c7a69cef18b ex/set.ML
--- a/ex/set.ML	Fri Jun 24 15:11:39 1994 +0200
+++ b/ex/set.ML	Wed Jun 29 12:04:04 1994 +0200
@@ -109,7 +109,7 @@
 by (fast_tac (set_cs addEs  [inj_ontoD, f_eq_gE]) 1);
 val bij_if_then_else = result();
 
-goal Lfp.thy "? X. X = Compl(g``Compl(f:: 'a=>'b``X))";
+goal Lfp.thy "? X. X = Compl(g``Compl((f:: 'a=>'b)``X))";
 by (rtac exI 1);
 by (rtac lfp_Tarski 1);
 by (REPEAT (ares_tac [monoI, image_mono, Compl_anti_mono] 1));
diff -r 5f462dfaf130 -r 5c7a69cef18b subset.ML
--- a/subset.ML	Fri Jun 24 15:11:39 1994 +0200
+++ b/subset.ML	Wed Jun 29 12:04:04 1994 +0200
@@ -117,7 +117,7 @@
 
 (*** Set difference ***)
 
-val Diff_subset = prove_goal Set.thy "A-B <= A::'a set"
+val Diff_subset = prove_goal Set.thy "A-B <= (A::'a set)"
  (fn _ => [ (REPEAT (ares_tac [subsetI] 1 ORELSE etac DiffE 1)) ]);
 
 (*** Monotonicity ***)