diff -r fb28eaa07e01 -r 3ea049f7979d src/HOL/Integ/Integ.ML
--- a/src/HOL/Integ/Integ.ML	Mon Jun 22 17:13:09 1998 +0200
+++ b/src/HOL/Integ/Integ.ML	Mon Jun 22 17:26:46 1998 +0200
@@ -39,7 +39,7 @@
 qed "intrelI";
 
 (*intrelE is hard to derive because fast_tac tries hyp_subst_tac so soon*)
-goalw Integ.thy [intrel_def]
+Goalw [intrel_def]
   "p: intrel --> (EX x1 y1 x2 y2. \
 \                  p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1)";
 by (Fast_tac 1);
@@ -56,15 +56,15 @@
 AddSIs [intrelI];
 AddSEs [intrelE];
 
-goal Integ.thy "((x1,y1),(x2,y2)): intrel = (x1+y2 = x2+y1)";
+Goal "((x1,y1),(x2,y2)): intrel = (x1+y2 = x2+y1)";
 by (Fast_tac 1);
 qed "intrel_iff";
 
-goal Integ.thy "(x,x): intrel";
+Goal "(x,x): intrel";
 by (stac surjective_pairing 1 THEN rtac (refl RS intrelI) 1);
 qed "intrel_refl";
 
-goalw Integ.thy [equiv_def, refl_def, sym_def, trans_def]
+Goalw [equiv_def, refl_def, sym_def, trans_def]
     "equiv {x::(nat*nat).True} intrel";
 by (fast_tac (claset() addSIs [intrel_refl] 
                         addSEs [sym, integ_trans_lemma]) 1);
@@ -75,11 +75,11 @@
     ([CollectI, CollectI] MRS 
     (equiv_intrel RS eq_equiv_class_iff));
 
-goalw Integ.thy  [Integ_def,intrel_def,quotient_def] "intrel^^{(x,y)}:Integ";
+Goalw  [Integ_def,intrel_def,quotient_def] "intrel^^{(x,y)}:Integ";
 by (Fast_tac 1);
 qed "intrel_in_integ";
 
-goal Integ.thy "inj_on Abs_Integ Integ";
+Goal "inj_on Abs_Integ Integ";
 by (rtac inj_on_inverseI 1);
 by (etac Abs_Integ_inverse 1);
 qed "inj_on_Abs_Integ";
@@ -87,7 +87,7 @@
 Addsimps [equiv_intrel_iff, inj_on_Abs_Integ RS inj_on_iff,
           intrel_iff, intrel_in_integ, Abs_Integ_inverse];
 
-goal Integ.thy "inj(Rep_Integ)";
+Goal "inj(Rep_Integ)";
 by (rtac inj_inverseI 1);
 by (rtac Rep_Integ_inverse 1);
 qed "inj_Rep_Integ";
@@ -97,7 +97,7 @@
 
 (** znat: the injection from nat to Integ **)
 
-goal Integ.thy "inj(znat)";
+Goal "inj(znat)";
 by (rtac injI 1);
 by (rewtac znat_def);
 by (dtac (inj_on_Abs_Integ RS inj_onD) 1);
@@ -112,7 +112,7 @@
 
 (**** zminus: unary negation on Integ ****)
 
-goalw Integ.thy [congruent_def]
+Goalw [congruent_def]
   "congruent intrel (%p. split (%x y. intrel^^{(y,x)}) p)";
 by Safe_tac;
 by (asm_simp_tac (simpset() addsimps add_ac) 1);
@@ -122,7 +122,7 @@
 (*Resolve th against the corresponding facts for zminus*)
 val zminus_ize = RSLIST [equiv_intrel, zminus_congruent];
 
-goalw Integ.thy [zminus_def]
+Goalw [zminus_def]
       "$~ Abs_Integ(intrel^^{(x,y)}) = Abs_Integ(intrel ^^ {(y,x)})";
 by (res_inst_tac [("f","Abs_Integ")] arg_cong 1);
 by (simp_tac (simpset() addsimps 
@@ -140,18 +140,18 @@
 by (asm_full_simp_tac (simpset() addsimps [Rep_Integ_inverse]) 1);
 qed "eq_Abs_Integ";
 
-goal Integ.thy "$~ ($~ z) = z";
+Goal "$~ ($~ z) = z";
 by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
 by (asm_simp_tac (simpset() addsimps [zminus]) 1);
 qed "zminus_zminus";
 
-goal Integ.thy "inj(zminus)";
+Goal "inj(zminus)";
 by (rtac injI 1);
 by (dres_inst_tac [("f","zminus")] arg_cong 1);
 by (asm_full_simp_tac (simpset() addsimps [zminus_zminus]) 1);
 qed "inj_zminus";
 
-goalw Integ.thy [znat_def] "$~ ($#0) = $#0";
+Goalw [znat_def] "$~ ($#0) = $#0";
 by (simp_tac (simpset() addsimps [zminus]) 1);
 qed "zminus_0";
 
@@ -159,13 +159,13 @@
 (**** znegative: the test for negative integers ****)
 
 
-goalw Integ.thy [znegative_def, znat_def]
+Goalw [znegative_def, znat_def]
     "~ znegative($# n)";
 by (Simp_tac 1);
 by Safe_tac;
 qed "not_znegative_znat";
 
-goalw Integ.thy [znegative_def, znat_def] "znegative($~ $# Suc(n))";
+Goalw [znegative_def, znat_def] "znegative($~ $# Suc(n))";
 by (simp_tac (simpset() addsimps [zminus]) 1);
 qed "znegative_zminus_znat";
 
@@ -182,7 +182,7 @@
 by (ALLGOALS Asm_simp_tac);
 qed "diff_Suc_add_inverse";
 
-goalw Integ.thy [congruent_def]
+Goalw [congruent_def]
     "congruent intrel (split (%x y. intrel^^{((y-x) + (x-(y::nat)),0)}))";
 by Safe_tac;
 by (Asm_simp_tac 1);
@@ -201,18 +201,18 @@
 val zmagnitude_ize = RSLIST [equiv_intrel, zmagnitude_congruent];
 
 
-goalw Integ.thy [zmagnitude_def]
+Goalw [zmagnitude_def]
     "zmagnitude (Abs_Integ(intrel^^{(x,y)})) = \
 \    Abs_Integ(intrel^^{((y - x) + (x - y),0)})";
 by (res_inst_tac [("f","Abs_Integ")] arg_cong 1);
 by (asm_simp_tac (simpset() addsimps [zmagnitude_ize UN_equiv_class]) 1);
 qed "zmagnitude";
 
-goalw Integ.thy [znat_def] "zmagnitude($# n) = $#n";
+Goalw [znat_def] "zmagnitude($# n) = $#n";
 by (asm_simp_tac (simpset() addsimps [zmagnitude]) 1);
 qed "zmagnitude_znat";
 
-goalw Integ.thy [znat_def] "zmagnitude($~ $# n) = $#n";
+Goalw [znat_def] "zmagnitude($~ $# n) = $#n";
 by (asm_simp_tac (simpset() addsimps [zmagnitude, zminus]) 1);
 qed "zmagnitude_zminus_znat";
 
@@ -221,7 +221,7 @@
 
 (** Congruence property for addition **)
 
-goalw Integ.thy [congruent2_def]
+Goalw [congruent2_def]
     "congruent2 intrel (%p1 p2.                  \
 \         split (%x1 y1. split (%x2 y2. intrel^^{(x1+x2, y1+y2)}) p2) p1)";
 (*Proof via congruent2_commuteI seems longer*)
@@ -235,31 +235,31 @@
 (*Resolve th against the corresponding facts for zadd*)
 val zadd_ize = RSLIST [equiv_intrel, zadd_congruent2];
 
-goalw Integ.thy [zadd_def]
+Goalw [zadd_def]
   "Abs_Integ(intrel^^{(x1,y1)}) + Abs_Integ(intrel^^{(x2,y2)}) = \
 \  Abs_Integ(intrel^^{(x1+x2, y1+y2)})";
 by (asm_simp_tac
     (simpset() addsimps [zadd_ize UN_equiv_class2]) 1);
 qed "zadd";
 
-goalw Integ.thy [znat_def] "$#0 + z = z";
+Goalw [znat_def] "$#0 + z = z";
 by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
 by (asm_simp_tac (simpset() addsimps [zadd]) 1);
 qed "zadd_0";
 
-goal Integ.thy "$~ (z + w) = $~ z + $~ w";
+Goal "$~ (z + w) = $~ z + $~ w";
 by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
 by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
 by (asm_simp_tac (simpset() addsimps [zminus,zadd]) 1);
 qed "zminus_zadd_distrib";
 
-goal Integ.thy "(z::int) + w = w + z";
+Goal "(z::int) + w = w + z";
 by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
 by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
 by (asm_simp_tac (simpset() addsimps (add_ac @ [zadd])) 1);
 qed "zadd_commute";
 
-goal Integ.thy "((z1::int) + z2) + z3 = z1 + (z2 + z3)";
+Goal "((z1::int) + z2) + z3 = z1 + (z2 + z3)";
 by (res_inst_tac [("z","z1")] eq_Abs_Integ 1);
 by (res_inst_tac [("z","z2")] eq_Abs_Integ 1);
 by (res_inst_tac [("z","z3")] eq_Abs_Integ 1);
@@ -267,7 +267,7 @@
 qed "zadd_assoc";
 
 (*For AC rewriting*)
-goal Integ.thy "(x::int)+(y+z)=y+(x+z)";
+Goal "(x::int)+(y+z)=y+(x+z)";
 by (rtac (zadd_commute RS trans) 1);
 by (rtac (zadd_assoc RS trans) 1);
 by (rtac (zadd_commute RS arg_cong) 1);
@@ -276,21 +276,21 @@
 (*Integer addition is an AC operator*)
 val zadd_ac = [zadd_assoc,zadd_commute,zadd_left_commute];
 
-goalw Integ.thy [znat_def] "$# (m + n) = ($#m) + ($#n)";
+Goalw [znat_def] "$# (m + n) = ($#m) + ($#n)";
 by (asm_simp_tac (simpset() addsimps [zadd]) 1);
 qed "znat_add";
 
-goalw Integ.thy [znat_def] "z + ($~ z) = $#0";
+Goalw [znat_def] "z + ($~ z) = $#0";
 by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
 by (asm_simp_tac (simpset() addsimps [zminus, zadd, add_commute]) 1);
 qed "zadd_zminus_inverse";
 
-goal Integ.thy "($~ z) + z = $#0";
+Goal "($~ z) + z = $#0";
 by (rtac (zadd_commute RS trans) 1);
 by (rtac zadd_zminus_inverse 1);
 qed "zadd_zminus_inverse2";
 
-goal Integ.thy "z + $#0 = z";
+Goal "z + $#0 = z";
 by (rtac (zadd_commute RS trans) 1);
 by (rtac zadd_0 1);
 qed "zadd_0_right";
@@ -312,11 +312,11 @@
 
 (** Congruence property for multiplication **)
 
-goal Integ.thy "((k::nat) + l) + (m + n) = (k + m) + (n + l)";
+Goal "((k::nat) + l) + (m + n) = (k + m) + (n + l)";
 by (simp_tac (simpset() addsimps add_ac) 1);
 qed "zmult_congruent_lemma";
 
-goal Integ.thy 
+Goal 
     "congruent2 intrel (%p1 p2.                 \
 \               split (%x1 y1. split (%x2 y2.   \
 \                   intrel^^{(x1*x2 + y1*y2, x1*y2 + y1*x2)}) p2) p1)";
@@ -340,50 +340,50 @@
 (*Resolve th against the corresponding facts for zmult*)
 val zmult_ize = RSLIST [equiv_intrel, zmult_congruent2];
 
-goalw Integ.thy [zmult_def]
+Goalw [zmult_def]
    "Abs_Integ((intrel^^{(x1,y1)})) * Abs_Integ((intrel^^{(x2,y2)})) =   \
 \   Abs_Integ(intrel ^^ {(x1*x2 + y1*y2, x1*y2 + y1*x2)})";
 by (simp_tac (simpset() addsimps [zmult_ize UN_equiv_class2]) 1);
 qed "zmult";
 
-goalw Integ.thy [znat_def] "$#0 * z = $#0";
+Goalw [znat_def] "$#0 * z = $#0";
 by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
 by (asm_simp_tac (simpset() addsimps [zmult]) 1);
 qed "zmult_0";
 
-goalw Integ.thy [znat_def] "$#Suc(0) * z = z";
+Goalw [znat_def] "$#Suc(0) * z = z";
 by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
 by (asm_simp_tac (simpset() addsimps [zmult]) 1);
 qed "zmult_1";
 
-goal Integ.thy "($~ z) * w = $~ (z * w)";
+Goal "($~ z) * w = $~ (z * w)";
 by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
 by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
 by (asm_simp_tac (simpset() addsimps ([zminus, zmult] @ add_ac)) 1);
 qed "zmult_zminus";
 
 
-goal Integ.thy "($~ z) * ($~ w) = (z * w)";
+Goal "($~ z) * ($~ w) = (z * w)";
 by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
 by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
 by (asm_simp_tac (simpset() addsimps ([zminus, zmult] @ add_ac)) 1);
 qed "zmult_zminus_zminus";
 
-goal Integ.thy "(z::int) * w = w * z";
+Goal "(z::int) * w = w * z";
 by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
 by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
 by (asm_simp_tac (simpset() addsimps ([zmult] @ add_ac @ mult_ac)) 1);
 qed "zmult_commute";
 
-goal Integ.thy "z * $# 0 = $#0";
+Goal "z * $# 0 = $#0";
 by (rtac ([zmult_commute, zmult_0] MRS trans) 1);
 qed "zmult_0_right";
 
-goal Integ.thy "z * $#Suc(0) = z";
+Goal "z * $#Suc(0) = z";
 by (rtac ([zmult_commute, zmult_1] MRS trans) 1);
 qed "zmult_1_right";
 
-goal Integ.thy "((z1::int) * z2) * z3 = z1 * (z2 * z3)";
+Goal "((z1::int) * z2) * z3 = z1 * (z2 * z3)";
 by (res_inst_tac [("z","z1")] eq_Abs_Integ 1);
 by (res_inst_tac [("z","z2")] eq_Abs_Integ 1);
 by (res_inst_tac [("z","z3")] eq_Abs_Integ 1);
@@ -400,7 +400,7 @@
 (*Integer multiplication is an AC operator*)
 val zmult_ac = [zmult_assoc, zmult_commute, zmult_left_commute];
 
-goal Integ.thy "((z1::int) + z2) * w = (z1 * w) + (z2 * w)";
+Goal "((z1::int) + z2) * w = (z1 * w) + (z2 * w)";
 by (res_inst_tac [("z","z1")] eq_Abs_Integ 1);
 by (res_inst_tac [("z","z2")] eq_Abs_Integ 1);
 by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
@@ -411,11 +411,11 @@
 
 val zmult_commute'= read_instantiate [("z","w")] zmult_commute;
 
-goal Integ.thy "w * ($~ z) = $~ (w * z)";
+Goal "w * ($~ z) = $~ (w * z)";
 by (simp_tac (simpset() addsimps [zmult_commute', zmult_zminus]) 1);
 qed "zmult_zminus_right";
 
-goal Integ.thy "(w::int) * (z1 + z2) = (w * z1) + (w * z2)";
+Goal "(w::int) * (z1 + z2) = (w * z1) + (w * z2)";
 by (simp_tac (simpset() addsimps [zmult_commute',zadd_zmult_distrib]) 1);
 qed "zadd_zmult_distrib2";
 
@@ -434,53 +434,53 @@
 (**** Additional Theorems (by Mattolini; proofs mainly by lcp) ****)
 
 (* Some Theorems about zsuc and zpred *)
-goalw Integ.thy [zsuc_def] "$#(Suc(n)) = zsuc($# n)";
+Goalw [zsuc_def] "$#(Suc(n)) = zsuc($# n)";
 by (simp_tac (simpset() addsimps [znat_add RS sym]) 1);
 qed "znat_Suc";
 
-goalw Integ.thy [zpred_def,zsuc_def,zdiff_def] "$~ zsuc(z) = zpred($~ z)";
+Goalw [zpred_def,zsuc_def,zdiff_def] "$~ zsuc(z) = zpred($~ z)";
 by (Simp_tac 1);
 qed "zminus_zsuc";
 
-goalw Integ.thy [zpred_def,zsuc_def,zdiff_def] "$~ zpred(z) = zsuc($~ z)";
+Goalw [zpred_def,zsuc_def,zdiff_def] "$~ zpred(z) = zsuc($~ z)";
 by (Simp_tac 1);
 qed "zminus_zpred";
 
-goalw Integ.thy [zsuc_def,zpred_def,zdiff_def]
+Goalw [zsuc_def,zpred_def,zdiff_def]
    "zpred(zsuc(z)) = z";
 by (simp_tac (simpset() addsimps [zadd_assoc]) 1);
 qed "zpred_zsuc";
 
-goalw Integ.thy [zsuc_def,zpred_def,zdiff_def]
+Goalw [zsuc_def,zpred_def,zdiff_def]
    "zsuc(zpred(z)) = z";
 by (simp_tac (simpset() addsimps [zadd_assoc]) 1);
 qed "zsuc_zpred";
 
-goal Integ.thy "(zpred(z)=w) = (z=zsuc(w))";
+Goal "(zpred(z)=w) = (z=zsuc(w))";
 by Safe_tac;
 by (rtac (zsuc_zpred RS sym) 1);
 by (rtac zpred_zsuc 1);
 qed "zpred_to_zsuc";
 
-goal Integ.thy "(zsuc(z)=w)=(z=zpred(w))";
+Goal "(zsuc(z)=w)=(z=zpred(w))";
 by Safe_tac;
 by (rtac (zpred_zsuc RS sym) 1);
 by (rtac zsuc_zpred 1);
 qed "zsuc_to_zpred";
 
-goal Integ.thy "($~ z = w) = (z = $~ w)";
+Goal "($~ z = w) = (z = $~ w)";
 by Safe_tac;
 by (rtac (zminus_zminus RS sym) 1);
 by (rtac zminus_zminus 1);
 qed "zminus_exchange";
 
-goal Integ.thy"(zsuc(z)=zsuc(w)) = (z=w)";
+Goal"(zsuc(z)=zsuc(w)) = (z=w)";
 by Safe_tac;
 by (dres_inst_tac [("f","zpred")] arg_cong 1);
 by (asm_full_simp_tac (simpset() addsimps [zpred_zsuc]) 1);
 qed "bijective_zsuc";
 
-goal Integ.thy"(zpred(z)=zpred(w)) = (z=w)";
+Goal"(zpred(z)=zpred(w)) = (z=w)";
 by Safe_tac;
 by (dres_inst_tac [("f","zsuc")] arg_cong 1);
 by (asm_full_simp_tac (simpset() addsimps [zsuc_zpred]) 1);
@@ -488,58 +488,58 @@
 
 (* Additional Theorems about zadd *)
 
-goalw Integ.thy [zsuc_def] "zsuc(z) + w = zsuc(z+w)";
+Goalw [zsuc_def] "zsuc(z) + w = zsuc(z+w)";
 by (simp_tac (simpset() addsimps zadd_ac) 1);
 qed "zadd_zsuc";
 
-goalw Integ.thy [zsuc_def] "w + zsuc(z) = zsuc(w+z)";
+Goalw [zsuc_def] "w + zsuc(z) = zsuc(w+z)";
 by (simp_tac (simpset() addsimps zadd_ac) 1);
 qed "zadd_zsuc_right";
 
-goalw Integ.thy [zpred_def,zdiff_def] "zpred(z) + w = zpred(z+w)";
+Goalw [zpred_def,zdiff_def] "zpred(z) + w = zpred(z+w)";
 by (simp_tac (simpset() addsimps zadd_ac) 1);
 qed "zadd_zpred";
 
-goalw Integ.thy [zpred_def,zdiff_def] "w + zpred(z) = zpred(w+z)";
+Goalw [zpred_def,zdiff_def] "w + zpred(z) = zpred(w+z)";
 by (simp_tac (simpset() addsimps zadd_ac) 1);
 qed "zadd_zpred_right";
 
 
 (* Additional Theorems about zmult *)
 
-goalw Integ.thy [zsuc_def] "zsuc(w) * z = z + w * z";
+Goalw [zsuc_def] "zsuc(w) * z = z + w * z";
 by (simp_tac (simpset() addsimps [zadd_zmult_distrib, zadd_commute]) 1);
 qed "zmult_zsuc";
 
-goalw Integ.thy [zsuc_def] "z * zsuc(w) = z + w * z";
+Goalw [zsuc_def] "z * zsuc(w) = z + w * z";
 by (simp_tac 
     (simpset() addsimps [zadd_zmult_distrib2, zadd_commute, zmult_commute]) 1);
 qed "zmult_zsuc_right";
 
-goalw Integ.thy [zpred_def, zdiff_def] "zpred(w) * z = w * z - z";
+Goalw [zpred_def, zdiff_def] "zpred(w) * z = w * z - z";
 by (simp_tac (simpset() addsimps [zadd_zmult_distrib]) 1);
 qed "zmult_zpred";
 
-goalw Integ.thy [zpred_def, zdiff_def] "z * zpred(w) = w * z - z";
+Goalw [zpred_def, zdiff_def] "z * zpred(w) = w * z - z";
 by (simp_tac (simpset() addsimps [zadd_zmult_distrib2, zmult_commute]) 1);
 qed "zmult_zpred_right";
 
 (* Further Theorems about zsuc and zpred *)
-goal Integ.thy "$#Suc(m) ~= $#0";
+Goal "$#Suc(m) ~= $#0";
 by (simp_tac (simpset() addsimps [inj_znat RS inj_eq]) 1);
 qed "znat_Suc_not_znat_Zero";
 
 bind_thm ("znat_Zero_not_znat_Suc", (znat_Suc_not_znat_Zero RS not_sym));
 
 
-goalw Integ.thy [zsuc_def,znat_def] "w ~= zsuc(w)";
+Goalw [zsuc_def,znat_def] "w ~= zsuc(w)";
 by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
 by (asm_full_simp_tac (simpset() addsimps [zadd]) 1);
 qed "n_not_zsuc_n";
 
 val zsuc_n_not_n = n_not_zsuc_n RS not_sym;
 
-goal Integ.thy "w ~= zpred(w)";
+Goal "w ~= zpred(w)";
 by Safe_tac;
 by (dres_inst_tac [("x","w"),("f","zsuc")] arg_cong 1);
 by (asm_full_simp_tac (simpset() addsimps [zsuc_zpred,zsuc_n_not_n]) 1);
@@ -550,7 +550,7 @@
 
 (* Theorems about less and less_equal *)
 
-goalw Integ.thy [zless_def, znegative_def, zdiff_def, znat_def] 
+Goalw [zless_def, znegative_def, zdiff_def, znat_def] 
     "!!w. w<z ==> ? n. z = w + $#(Suc(n))";
 by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
 by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
@@ -561,26 +561,26 @@
 by (asm_full_simp_tac (simpset() addsimps add_ac) 1);
 qed "zless_eq_zadd_Suc";
 
-goalw Integ.thy [zless_def, znegative_def, zdiff_def, znat_def] 
+Goalw [zless_def, znegative_def, zdiff_def, znat_def] 
     "z < z + $#(Suc(n))";
 by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
 by (Clarify_tac 1);
 by (simp_tac (simpset() addsimps [zadd, zminus]) 1);
 qed "zless_zadd_Suc";
 
-goal Integ.thy "!!z1 z2 z3. [| z1<z2; z2<z3 |] ==> z1 < (z3::int)";
+Goal "!!z1 z2 z3. [| z1<z2; z2<z3 |] ==> z1 < (z3::int)";
 by (safe_tac (claset() addSDs [zless_eq_zadd_Suc]));
 by (simp_tac 
     (simpset() addsimps [zadd_assoc, zless_zadd_Suc, znat_add RS sym]) 1);
 qed "zless_trans";
 
-goalw Integ.thy [zsuc_def] "z<zsuc(z)";
+Goalw [zsuc_def] "z<zsuc(z)";
 by (rtac zless_zadd_Suc 1);
 qed "zlessI";
 
 val zless_zsucI = zlessI RSN (2,zless_trans);
 
-goal Integ.thy "!!z w::int. z<w ==> ~w<z";
+Goal "!!z w::int. z<w ==> ~w<z";
 by (safe_tac (claset() addSDs [zless_eq_zadd_Suc]));
 by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
 by Safe_tac;
@@ -590,7 +590,7 @@
 (* [| n<m; m<n |] ==> R *)
 bind_thm ("zless_asym", (zless_not_sym RS notE));
 
-goal Integ.thy "!!z::int. ~ z<z";
+Goal "!!z::int. ~ z<z";
 by (resolve_tac [zless_asym RS notI] 1);
 by (REPEAT (assume_tac 1));
 qed "zless_not_refl";
@@ -598,13 +598,13 @@
 (* z<z ==> R *)
 bind_thm ("zless_irrefl", (zless_not_refl RS notE));
 
-goal Integ.thy "!!w. z<w ==> w ~= (z::int)";
+Goal "!!w. z<w ==> w ~= (z::int)";
 by (fast_tac (claset() addEs [zless_irrefl]) 1);
 qed "zless_not_refl2";
 
 
 (*"Less than" is a linear ordering*)
-goalw Integ.thy [zless_def, znegative_def, zdiff_def] 
+Goalw [zless_def, znegative_def, zdiff_def] 
     "z<w | z=w | w<(z::int)";
 by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
 by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
@@ -618,50 +618,50 @@
 
 (*** Properties of <= ***)
 
-goalw Integ.thy  [zless_def, znegative_def, zdiff_def, znat_def]
+Goalw  [zless_def, znegative_def, zdiff_def, znat_def]
     "($#m < $#n) = (m<n)";
 by (simp_tac
     (simpset() addsimps [zadd, zminus, Image_iff, Bex_def]) 1);
 by (fast_tac (claset() addIs [add_commute] addSEs [less_add_eq_less]) 1);
 qed "zless_eq_less";
 
-goalw Integ.thy [zle_def, le_def] "($#m <= $#n) = (m<=n)";
+Goalw [zle_def, le_def] "($#m <= $#n) = (m<=n)";
 by (simp_tac (simpset() addsimps [zless_eq_less]) 1);
 qed "zle_eq_le";
 
-goalw Integ.thy [zle_def] "!!w. ~(w<z) ==> z<=(w::int)";
+Goalw [zle_def] "!!w. ~(w<z) ==> z<=(w::int)";
 by (assume_tac 1);
 qed "zleI";
 
-goalw Integ.thy [zle_def] "!!w. z<=w ==> ~(w<(z::int))";
+Goalw [zle_def] "!!w. z<=w ==> ~(w<(z::int))";
 by (assume_tac 1);
 qed "zleD";
 
 val zleE = make_elim zleD;
 
-goalw Integ.thy [zle_def] "!!z. ~ z <= w ==> w<(z::int)";
+Goalw [zle_def] "!!z. ~ z <= w ==> w<(z::int)";
 by (Fast_tac 1);
 qed "not_zleE";
 
-goalw Integ.thy [zle_def] "!!z. z < w ==> z <= (w::int)";
+Goalw [zle_def] "!!z. z < w ==> z <= (w::int)";
 by (fast_tac (claset() addEs [zless_asym]) 1);
 qed "zless_imp_zle";
 
-goalw Integ.thy [zle_def] "!!z. z <= w ==> z < w | z=(w::int)";
+Goalw [zle_def] "!!z. z <= w ==> z < w | z=(w::int)";
 by (cut_facts_tac [zless_linear] 1);
 by (fast_tac (claset() addEs [zless_irrefl,zless_asym]) 1);
 qed "zle_imp_zless_or_eq";
 
-goalw Integ.thy [zle_def] "!!z. z<w | z=w ==> z <=(w::int)";
+Goalw [zle_def] "!!z. z<w | z=w ==> z <=(w::int)";
 by (cut_facts_tac [zless_linear] 1);
 by (fast_tac (claset() addEs [zless_irrefl,zless_asym]) 1);
 qed "zless_or_eq_imp_zle";
 
-goal Integ.thy "(x <= (y::int)) = (x < y | x=y)";
+Goal "(x <= (y::int)) = (x < y | x=y)";
 by (REPEAT(ares_tac [iffI, zless_or_eq_imp_zle, zle_imp_zless_or_eq] 1));
 qed "zle_eq_zless_or_eq";
 
-goal Integ.thy "w <= (w::int)";
+Goal "w <= (w::int)";
 by (simp_tac (simpset() addsimps [zle_eq_zless_or_eq]) 1);
 qed "zle_refl";
 
@@ -670,18 +670,18 @@
 by (fast_tac (claset() addIs [zless_trans]) 1);
 qed "zle_zless_trans";
 
-goal Integ.thy "!!i. [| i <= j; j <= k |] ==> i <= (k::int)";
+Goal "!!i. [| i <= j; j <= k |] ==> i <= (k::int)";
 by (EVERY1 [dtac zle_imp_zless_or_eq, dtac zle_imp_zless_or_eq,
             rtac zless_or_eq_imp_zle, fast_tac (claset() addIs [zless_trans])]);
 qed "zle_trans";
 
-goal Integ.thy "!!z. [| z <= w; w <= z |] ==> z = (w::int)";
+Goal "!!z. [| z <= w; w <= z |] ==> z = (w::int)";
 by (EVERY1 [dtac zle_imp_zless_or_eq, dtac zle_imp_zless_or_eq,
             fast_tac (claset() addEs [zless_irrefl,zless_asym])]);
 qed "zle_anti_sym";
 
 
-goal Integ.thy "!!w w' z::int. z + w' = z + w ==> w' = w";
+Goal "!!w w' z::int. z + w' = z + w ==> w' = w";
 by (dres_inst_tac [("f", "%x. x + $~z")] arg_cong 1);
 by (asm_full_simp_tac (simpset() addsimps zadd_ac) 1);
 qed "zadd_left_cancel";
@@ -689,19 +689,19 @@
 
 (*** Monotonicity results ***)
 
-goal Integ.thy "!!v w z::int. v < w ==> v + z < w + z";
+Goal "!!v w z::int. v < w ==> v + z < w + z";
 by (safe_tac (claset() addSDs [zless_eq_zadd_Suc]));
 by (simp_tac (simpset() addsimps zadd_ac) 1);
 by (simp_tac (simpset() addsimps [zadd_assoc RS sym, zless_zadd_Suc]) 1);
 qed "zadd_zless_mono1";
 
-goal Integ.thy "!!v w z::int. (v+z < w+z) = (v < w)";
+Goal "!!v w z::int. (v+z < w+z) = (v < w)";
 by (safe_tac (claset() addSEs [zadd_zless_mono1]));
 by (dres_inst_tac [("z", "$~z")] zadd_zless_mono1 1);
 by (asm_full_simp_tac (simpset() addsimps [zadd_assoc]) 1);
 qed "zadd_left_cancel_zless";
 
-goal Integ.thy "!!v w z::int. (v+z <= w+z) = (v <= w)";
+Goal "!!v w z::int. (v+z <= w+z) = (v <= w)";
 by (asm_full_simp_tac
     (simpset() addsimps [zle_def, zadd_left_cancel_zless]) 1);
 qed "zadd_left_cancel_zle";
@@ -710,14 +710,14 @@
 bind_thm ("zadd_zle_mono1", zadd_left_cancel_zle RS iffD2);
 
 
-goal Integ.thy "!!z' z::int. [| w'<=w; z'<=z |] ==> w' + z' <= w + z";
+Goal "!!z' z::int. [| w'<=w; z'<=z |] ==> w' + z' <= w + z";
 by (etac (zadd_zle_mono1 RS zle_trans) 1);
 by (simp_tac (simpset() addsimps [zadd_commute]) 1);
 (*w moves to the end because it is free while z', z are bound*)
 by (etac zadd_zle_mono1 1);
 qed "zadd_zle_mono";
 
-goal Integ.thy "!!w z::int. z<=$#0 ==> w+z <= w";
+Goal "!!w z::int. z<=$#0 ==> w+z <= w";
 by (dres_inst_tac [("z", "w")] zadd_zle_mono1 1);
 by (asm_full_simp_tac (simpset() addsimps [zadd_commute]) 1);
 qed "zadd_zle_self";
@@ -736,67 +736,67 @@
 Addsimps [zless_eq_less, zle_eq_le,
 	  znegative_zminus_znat, not_znegative_znat]; 
 
-goal Integ.thy "!! x. (x::int) = y ==> x <= y"; 
+Goal "!! x. (x::int) = y ==> x <= y"; 
   by (etac subst 1); by (rtac zle_refl 1); 
 qed "zequalD1"; 
 
-goal Integ.thy "($~ x < $~ y) = (y < x)";
+Goal "($~ x < $~ y) = (y < x)";
   by (rewrite_goals_tac [zless_def,zdiff_def]); 
   by (simp_tac (simpset() addsimps zadd_ac ) 1); 
 qed "zminus_zless_zminus"; 
 
-goal Integ.thy "($~ x <= $~ y) = (y <= x)";
+Goal "($~ x <= $~ y) = (y <= x)";
   by (simp_tac (HOL_ss addsimps[zle_def, zminus_zless_zminus]) 1); 
 qed "zminus_zle_zminus"; 
 
-goal Integ.thy "(x < $~ y) = (y < $~ x)";
+Goal "(x < $~ y) = (y < $~ x)";
   by (rewrite_goals_tac [zless_def,zdiff_def]); 
   by (simp_tac (simpset() addsimps zadd_ac ) 1); 
 qed "zless_zminus"; 
 
-goal Integ.thy "($~ x < y) = ($~ y < x)";
+Goal "($~ x < y) = ($~ y < x)";
   by (rewrite_goals_tac [zless_def,zdiff_def]); 
   by (simp_tac (simpset() addsimps zadd_ac ) 1); 
 qed "zminus_zless"; 
 
-goal Integ.thy "(x <= $~ y) = (y <=  $~ x)";
+Goal "(x <= $~ y) = (y <=  $~ x)";
   by (simp_tac (HOL_ss addsimps[zle_def, zminus_zless]) 1); 
 qed "zle_zminus"; 
 
-goal Integ.thy "($~ x <= y) = ($~ y <=  x)";
+Goal "($~ x <= y) = ($~ y <=  x)";
   by (simp_tac (HOL_ss addsimps[zle_def, zless_zminus]) 1); 
 qed "zminus_zle"; 
 
-goal Integ.thy " $#0 < $# Suc n"; 
+Goal " $#0 < $# Suc n"; 
   by (rtac (zero_less_Suc RS (zless_eq_less RS iffD2)) 1); 
 qed "zero_zless_Suc_pos"; 
 
-goal Integ.thy "($# n= $# m) = (n = m)"; 
+Goal "($# n= $# m) = (n = m)"; 
   by (fast_tac (HOL_cs addSEs[inj_znat RS injD]) 1); 
 qed "znat_znat_eq"; 
 AddIffs[znat_znat_eq]; 
 
-goal Integ.thy "$~ $# Suc n < $#0";
+Goal "$~ $# Suc n < $#0";
   by (stac (zminus_0 RS sym) 1); 
   by (rtac (zminus_zless_zminus RS iffD2) 1); 
   by (rtac (zero_less_Suc RS (zless_eq_less RS iffD2)) 1); 
 qed "negative_zless_0"; 
 Addsimps [zero_zless_Suc_pos, negative_zless_0]; 
 
-goal Integ.thy "$~ $#  n <= $#0";
+Goal "$~ $#  n <= $#0";
   by (rtac zless_or_eq_imp_zle 1); 
   by (nat_ind_tac "n" 1); 
   by (ALLGOALS Asm_simp_tac); 
 qed "negative_zle_0"; 
 Addsimps[negative_zle_0]; 
 
-goal Integ.thy "~($#0 <= $~ $# Suc n)";
+Goal "~($#0 <= $~ $# Suc n)";
   by (stac zle_zminus 1);
   by (Simp_tac 1);
 qed "not_zle_0_negative"; 
 Addsimps[not_zle_0_negative]; 
 
-goal Integ.thy "($# n <= $~ $# m) = (n = 0 & m = 0)"; 
+Goal "($# n <= $~ $# m) = (n = 0 & m = 0)"; 
   by (safe_tac HOL_cs); 
   by (Simp_tac 3); 
   by (dtac (zle_zminus RS iffD1) 2); 
@@ -804,7 +804,7 @@
   by (ALLGOALS Asm_full_simp_tac); 
 qed "znat_zle_znegative"; 
 
-goal Integ.thy "~($# n < $~ $# Suc m)";
+Goal "~($# n < $~ $# Suc m)";
   by (rtac notI 1); by (forward_tac [zless_imp_zle] 1); 
   by (dtac (znat_zle_znegative RS iffD1) 1); 
   by (safe_tac HOL_cs); 
@@ -812,7 +812,7 @@
   by (Asm_full_simp_tac 1);
 qed "not_znat_zless_negative"; 
 
-goal Integ.thy "($~ $# n = $# m) = (n = 0 & m = 0)"; 
+Goal "($~ $# n = $# m) = (n = 0 & m = 0)"; 
   by (rtac iffI 1);
   by (rtac  (znat_zle_znegative RS iffD1) 1); 
   by (dtac sym 1); 
@@ -822,16 +822,16 @@
 Addsimps [zminus_zless_zminus, zminus_zle_zminus, 
 	  negative_eq_positive, not_znat_zless_negative]; 
 
-goalw Integ.thy [zdiff_def,zless_def] "!! x. znegative x = (x < $# 0)";
+Goalw [zdiff_def,zless_def] "!! x. znegative x = (x < $# 0)";
   by Auto_tac; 
 qed "znegative_less_0"; 
 
-goalw Integ.thy [zdiff_def,zless_def] "!! x. (~znegative x) = ($# 0 <= x)";
+Goalw [zdiff_def,zless_def] "!! x. (~znegative x) = ($# 0 <= x)";
   by (stac znegative_less_0 1); 
   by (safe_tac (HOL_cs addSDs[zleD,not_zleE,zleI]) ); 
 qed "not_znegative_ge_0"; 
 
-goal Integ.thy "!! x. znegative x ==> ? n. x = $~ $# Suc n"; 
+Goal "!! x. znegative x ==> ? n. x = $~ $# Suc n"; 
   by (dtac (znegative_less_0 RS iffD1 RS zless_eq_zadd_Suc) 1); 
   by (etac exE 1); 
   by (rtac exI 1);
@@ -839,7 +839,7 @@
   by (auto_tac(claset(), simpset() addsimps [zadd_assoc])); 
 qed "znegativeD"; 
 
-goal Integ.thy "!! x. ~znegative x ==> ? n. x = $# n"; 
+Goal "!! x. ~znegative x ==> ? n. x = $# n"; 
   by (dtac (not_znegative_ge_0 RS iffD1) 1); 
   by (dtac zle_imp_zless_or_eq 1); 
   by (etac disjE 1);