added local simpsets; removed IOA from 'make test'
authorclasohm
Wed Oct 04 13:10:03 1995 +0100 (1995-10-04)
changeset 12643eb91524b938
parent 1263 290c4dfc34ba
child 1265 6ef9a9893fd6
added local simpsets; removed IOA from 'make test'
src/HOL/Arith.ML
src/HOL/Finite.ML
src/HOL/Fun.ML
src/HOL/Lfp.ML
src/HOL/Lfp.thy
src/HOL/List.ML
src/HOL/Makefile
src/HOL/Nat.ML
src/HOL/Prod.ML
src/HOL/ROOT.ML
src/HOL/Relation.ML
src/HOL/Sexp.ML
src/HOL/Sum.ML
src/HOL/Univ.ML
src/HOL/WF.ML
src/HOL/equalities.ML
src/HOL/indrule.ML
src/HOL/intr_elim.ML
src/HOL/mono.ML
src/HOL/mono.thy
src/HOL/simpdata.ML
src/HOL/subtype.ML
src/HOL/thy_syntax.ML
src/HOL/typedef.ML
     1.1 --- a/src/HOL/Arith.ML	Wed Oct 04 13:01:05 1995 +0100
     1.2 +++ b/src/HOL/Arith.ML	Wed Oct 04 13:10:03 1995 +0100
     1.3 @@ -21,42 +21,40 @@
     1.4  
     1.5  qed_goalw "diff_0_eq_0" Arith.thy [diff_def, pred_def]
     1.6      "0 - n = 0"
     1.7 - (fn _ => [nat_ind_tac "n" 1,  ALLGOALS(asm_simp_tac nat_ss)]);
     1.8 + (fn _ => [nat_ind_tac "n" 1,  ALLGOALS Asm_simp_tac]);
     1.9  
    1.10  (*Must simplify BEFORE the induction!!  (Else we get a critical pair)
    1.11    Suc(m) - Suc(n)   rewrites to   pred(Suc(m) - n)  *)
    1.12  qed_goalw "diff_Suc_Suc" Arith.thy [diff_def, pred_def]
    1.13      "Suc(m) - Suc(n) = m - n"
    1.14   (fn _ =>
    1.15 -  [simp_tac nat_ss 1, nat_ind_tac "n" 1, ALLGOALS(asm_simp_tac nat_ss)]);
    1.16 +  [Simp_tac 1, nat_ind_tac "n" 1, ALLGOALS Asm_simp_tac]);
    1.17  
    1.18  (*** Simplification over add, mult, diff ***)
    1.19  
    1.20 -val arith_simps =
    1.21 - [pred_0, pred_Suc, add_0, add_Suc, mult_0, mult_Suc,
    1.22 -  diff_0, diff_0_eq_0, diff_Suc_Suc];
    1.23 +Addsimps [pred_0, pred_Suc, add_0, add_Suc, mult_0, mult_Suc, diff_0,
    1.24 +          diff_0_eq_0, diff_Suc_Suc];
    1.25  
    1.26 -val arith_ss = nat_ss addsimps arith_simps;
    1.27  
    1.28  (**** Inductive properties of the operators ****)
    1.29  
    1.30  (*** Addition ***)
    1.31  
    1.32  qed_goal "add_0_right" Arith.thy "m + 0 = m"
    1.33 - (fn _ => [nat_ind_tac "m" 1, ALLGOALS(asm_simp_tac arith_ss)]);
    1.34 + (fn _ => [nat_ind_tac "m" 1, ALLGOALS Asm_simp_tac]);
    1.35  
    1.36  qed_goal "add_Suc_right" Arith.thy "m + Suc(n) = Suc(m+n)"
    1.37 - (fn _ => [nat_ind_tac "m" 1, ALLGOALS(asm_simp_tac arith_ss)]);
    1.38 + (fn _ => [nat_ind_tac "m" 1, ALLGOALS Asm_simp_tac]);
    1.39  
    1.40 -val arith_ss = arith_ss addsimps [add_0_right,add_Suc_right];
    1.41 +Addsimps [add_0_right,add_Suc_right];
    1.42  
    1.43  (*Associative law for addition*)
    1.44  qed_goal "add_assoc" Arith.thy "(m + n) + k = m + ((n + k)::nat)"
    1.45 - (fn _ => [nat_ind_tac "m" 1, ALLGOALS(asm_simp_tac arith_ss)]);
    1.46 + (fn _ => [nat_ind_tac "m" 1, ALLGOALS Asm_simp_tac]);
    1.47  
    1.48  (*Commutative law for addition*)  
    1.49  qed_goal "add_commute" Arith.thy "m + n = n + (m::nat)"
    1.50 - (fn _ =>  [nat_ind_tac "m" 1, ALLGOALS(asm_simp_tac arith_ss)]);
    1.51 + (fn _ =>  [nat_ind_tac "m" 1, ALLGOALS Asm_simp_tac]);
    1.52  
    1.53  qed_goal "add_left_commute" Arith.thy "x+(y+z)=y+((x+z)::nat)"
    1.54   (fn _ => [rtac (add_commute RS trans) 1, rtac (add_assoc RS trans) 1,
    1.55 @@ -67,59 +65,59 @@
    1.56  
    1.57  goal Arith.thy "!!k::nat. (k + m = k + n) = (m=n)";
    1.58  by (nat_ind_tac "k" 1);
    1.59 -by (simp_tac arith_ss 1);
    1.60 -by (asm_simp_tac arith_ss 1);
    1.61 +by (Simp_tac 1);
    1.62 +by (Asm_simp_tac 1);
    1.63  qed "add_left_cancel";
    1.64  
    1.65  goal Arith.thy "!!k::nat. (m + k = n + k) = (m=n)";
    1.66  by (nat_ind_tac "k" 1);
    1.67 -by (simp_tac arith_ss 1);
    1.68 -by (asm_simp_tac arith_ss 1);
    1.69 +by (Simp_tac 1);
    1.70 +by (Asm_simp_tac 1);
    1.71  qed "add_right_cancel";
    1.72  
    1.73  goal Arith.thy "!!k::nat. (k + m <= k + n) = (m<=n)";
    1.74  by (nat_ind_tac "k" 1);
    1.75 -by (simp_tac arith_ss 1);
    1.76 -by (asm_simp_tac (arith_ss addsimps [Suc_le_mono]) 1);
    1.77 +by (Simp_tac 1);
    1.78 +by (Asm_simp_tac 1);
    1.79  qed "add_left_cancel_le";
    1.80  
    1.81  goal Arith.thy "!!k::nat. (k + m < k + n) = (m<n)";
    1.82  by (nat_ind_tac "k" 1);
    1.83 -by (simp_tac arith_ss 1);
    1.84 -by (asm_simp_tac arith_ss 1);
    1.85 +by (Simp_tac 1);
    1.86 +by (Asm_simp_tac 1);
    1.87  qed "add_left_cancel_less";
    1.88  
    1.89  (*** Multiplication ***)
    1.90  
    1.91  (*right annihilation in product*)
    1.92  qed_goal "mult_0_right" Arith.thy "m * 0 = 0"
    1.93 - (fn _ => [nat_ind_tac "m" 1, ALLGOALS(asm_simp_tac arith_ss)]);
    1.94 + (fn _ => [nat_ind_tac "m" 1, ALLGOALS Asm_simp_tac]);
    1.95  
    1.96  (*right Sucessor law for multiplication*)
    1.97  qed_goal "mult_Suc_right" Arith.thy  "m * Suc(n) = m + (m * n)"
    1.98   (fn _ => [nat_ind_tac "m" 1,
    1.99 -           ALLGOALS(asm_simp_tac (arith_ss addsimps add_ac))]);
   1.100 +           ALLGOALS(asm_simp_tac (!simpset addsimps add_ac))]);
   1.101  
   1.102 -val arith_ss = arith_ss addsimps [mult_0_right,mult_Suc_right];
   1.103 +Addsimps [mult_0_right,mult_Suc_right];
   1.104  
   1.105  (*Commutative law for multiplication*)
   1.106  qed_goal "mult_commute" Arith.thy "m * n = n * (m::nat)"
   1.107 - (fn _ => [nat_ind_tac "m" 1, ALLGOALS (asm_simp_tac arith_ss)]);
   1.108 + (fn _ => [nat_ind_tac "m" 1, ALLGOALS Asm_simp_tac]);
   1.109  
   1.110  (*addition distributes over multiplication*)
   1.111  qed_goal "add_mult_distrib" Arith.thy "(m + n)*k = (m*k) + ((n*k)::nat)"
   1.112   (fn _ => [nat_ind_tac "m" 1,
   1.113 -           ALLGOALS(asm_simp_tac (arith_ss addsimps add_ac))]);
   1.114 +           ALLGOALS(asm_simp_tac (!simpset addsimps add_ac))]);
   1.115  
   1.116  qed_goal "add_mult_distrib2" Arith.thy "k*(m + n) = (k*m) + ((k*n)::nat)"
   1.117   (fn _ => [nat_ind_tac "m" 1,
   1.118 -           ALLGOALS(asm_simp_tac (arith_ss addsimps add_ac))]);
   1.119 +           ALLGOALS(asm_simp_tac (!simpset addsimps add_ac))]);
   1.120  
   1.121 -val arith_ss = arith_ss addsimps [add_mult_distrib,add_mult_distrib2];
   1.122 +Addsimps [add_mult_distrib,add_mult_distrib2];
   1.123  
   1.124  (*Associative law for multiplication*)
   1.125  qed_goal "mult_assoc" Arith.thy "(m * n) * k = m * ((n * k)::nat)"
   1.126 -  (fn _ => [nat_ind_tac "m" 1, ALLGOALS(asm_simp_tac arith_ss)]);
   1.127 +  (fn _ => [nat_ind_tac "m" 1, ALLGOALS Asm_simp_tac]);
   1.128  
   1.129  qed_goal "mult_left_commute" Arith.thy "x*(y*z) = y*((x*z)::nat)"
   1.130   (fn _ => [rtac trans 1, rtac mult_commute 1, rtac trans 1,
   1.131 @@ -130,13 +128,13 @@
   1.132  (*** Difference ***)
   1.133  
   1.134  qed_goal "diff_self_eq_0" Arith.thy "m - m = 0"
   1.135 - (fn _ => [nat_ind_tac "m" 1, ALLGOALS(asm_simp_tac arith_ss)]);
   1.136 + (fn _ => [nat_ind_tac "m" 1, ALLGOALS Asm_simp_tac]);
   1.137  
   1.138  (*Addition is the inverse of subtraction: if n<=m then n+(m-n) = m. *)
   1.139  val [prem] = goal Arith.thy "[| ~ m<n |] ==> n+(m-n) = (m::nat)";
   1.140  by (rtac (prem RS rev_mp) 1);
   1.141  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   1.142 -by (ALLGOALS(asm_simp_tac arith_ss));
   1.143 +by (ALLGOALS Asm_simp_tac);
   1.144  qed "add_diff_inverse";
   1.145  
   1.146  
   1.147 @@ -145,24 +143,24 @@
   1.148  goal Arith.thy "m - n < Suc(m)";
   1.149  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   1.150  by (etac less_SucE 3);
   1.151 -by (ALLGOALS(asm_simp_tac arith_ss));
   1.152 +by (ALLGOALS Asm_simp_tac);
   1.153  qed "diff_less_Suc";
   1.154  
   1.155  goal Arith.thy "!!m::nat. m - n <= m";
   1.156  by (res_inst_tac [("m","m"), ("n","n")] diff_induct 1);
   1.157 -by (ALLGOALS (asm_simp_tac arith_ss));
   1.158 +by (ALLGOALS Asm_simp_tac);
   1.159  by (etac le_trans 1);
   1.160 -by (simp_tac (HOL_ss addsimps [le_eq_less_or_eq, lessI]) 1);
   1.161 +by (simp_tac (!simpset addsimps [le_eq_less_or_eq]) 1);
   1.162  qed "diff_le_self";
   1.163  
   1.164  goal Arith.thy "!!n::nat. (n+m) - n = m";
   1.165  by (nat_ind_tac "n" 1);
   1.166 -by (ALLGOALS (asm_simp_tac arith_ss));
   1.167 +by (ALLGOALS Asm_simp_tac);
   1.168  qed "diff_add_inverse";
   1.169  
   1.170  goal Arith.thy "!!n::nat. n - (n+m) = 0";
   1.171  by (nat_ind_tac "n" 1);
   1.172 -by (ALLGOALS (asm_simp_tac arith_ss));
   1.173 +by (ALLGOALS Asm_simp_tac);
   1.174  qed "diff_add_0";
   1.175  
   1.176  (*In ordinary notation: if 0<n and n<=m then m-n < m *)
   1.177 @@ -170,7 +168,7 @@
   1.178  by (subgoal_tac "0<n --> ~ m<n --> m - n < m" 1);
   1.179  by (fast_tac HOL_cs 1);
   1.180  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   1.181 -by (ALLGOALS(asm_simp_tac(arith_ss addsimps [diff_less_Suc])));
   1.182 +by (ALLGOALS(asm_simp_tac(!simpset addsimps [diff_less_Suc])));
   1.183  qed "div_termination";
   1.184  
   1.185  val wf_less_trans = wf_pred_nat RS wf_trancl RSN (2, def_wfrec RS trans);
   1.186 @@ -181,12 +179,12 @@
   1.187  
   1.188  goal Arith.thy "!!m. m<n ==> m mod n = m";
   1.189  by (rtac (mod_def RS wf_less_trans) 1);
   1.190 -by(asm_simp_tac HOL_ss 1);
   1.191 +by(Asm_simp_tac 1);
   1.192  qed "mod_less";
   1.193  
   1.194  goal Arith.thy "!!m. [| 0<n;  ~m<n |] ==> m mod n = (m-n) mod n";
   1.195  by (rtac (mod_def RS wf_less_trans) 1);
   1.196 -by(asm_simp_tac (nat_ss addsimps [div_termination, cut_apply, less_eq]) 1);
   1.197 +by(asm_simp_tac (!simpset addsimps [div_termination, cut_apply, less_eq]) 1);
   1.198  qed "mod_geq";
   1.199  
   1.200  
   1.201 @@ -194,12 +192,12 @@
   1.202  
   1.203  goal Arith.thy "!!m. m<n ==> m div n = 0";
   1.204  by (rtac (div_def RS wf_less_trans) 1);
   1.205 -by(asm_simp_tac nat_ss 1);
   1.206 +by(Asm_simp_tac 1);
   1.207  qed "div_less";
   1.208  
   1.209  goal Arith.thy "!!M. [| 0<n;  ~m<n |] ==> m div n = Suc((m-n) div n)";
   1.210  by (rtac (div_def RS wf_less_trans) 1);
   1.211 -by(asm_simp_tac (nat_ss addsimps [div_termination, cut_apply, less_eq]) 1);
   1.212 +by(asm_simp_tac (!simpset addsimps [div_termination, cut_apply, less_eq]) 1);
   1.213  qed "div_geq";
   1.214  
   1.215  (*Main Result about quotient and remainder.*)
   1.216 @@ -207,7 +205,7 @@
   1.217  by (res_inst_tac [("n","m")] less_induct 1);
   1.218  by (rename_tac "k" 1);    (*Variable name used in line below*)
   1.219  by (case_tac "k<n" 1);
   1.220 -by (ALLGOALS (asm_simp_tac(arith_ss addsimps (add_ac @
   1.221 +by (ALLGOALS (asm_simp_tac(!simpset addsimps (add_ac @
   1.222                         [mod_less, mod_geq, div_less, div_geq,
   1.223  	                add_diff_inverse, div_termination]))));
   1.224  qed "mod_div_equality";
   1.225 @@ -218,12 +216,12 @@
   1.226  val [prem] = goal Arith.thy "m < Suc(n) ==> m-n = 0";
   1.227  by (rtac (prem RS rev_mp) 1);
   1.228  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   1.229 -by (ALLGOALS (asm_simp_tac arith_ss));
   1.230 +by (ALLGOALS Asm_simp_tac);
   1.231  qed "less_imp_diff_is_0";
   1.232  
   1.233  val prems = goal Arith.thy "m-n = 0  -->  n-m = 0  -->  m=n";
   1.234  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   1.235 -by (REPEAT(simp_tac arith_ss 1 THEN TRY(atac 1)));
   1.236 +by (REPEAT(Simp_tac 1 THEN TRY(atac 1)));
   1.237  qed "diffs0_imp_equal_lemma";
   1.238  
   1.239  (*  [| m-n = 0;  n-m = 0 |] ==> m=n  *)
   1.240 @@ -232,23 +230,23 @@
   1.241  val [prem] = goal Arith.thy "m<n ==> 0<n-m";
   1.242  by (rtac (prem RS rev_mp) 1);
   1.243  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   1.244 -by (ALLGOALS(asm_simp_tac arith_ss));
   1.245 +by (ALLGOALS Asm_simp_tac);
   1.246  qed "less_imp_diff_positive";
   1.247  
   1.248  val [prem] = goal Arith.thy "n < Suc(m) ==> Suc(m)-n = Suc(m-n)";
   1.249  by (rtac (prem RS rev_mp) 1);
   1.250  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   1.251 -by (ALLGOALS(asm_simp_tac arith_ss));
   1.252 +by (ALLGOALS Asm_simp_tac);
   1.253  qed "Suc_diff_n";
   1.254  
   1.255  goal Arith.thy "Suc(m)-n = (if m<n then 0 else Suc m-n)";
   1.256 -by(simp_tac (nat_ss addsimps [less_imp_diff_is_0, not_less_eq, Suc_diff_n]
   1.257 +by(simp_tac (!simpset addsimps [less_imp_diff_is_0, not_less_eq, Suc_diff_n]
   1.258                      setloop (split_tac [expand_if])) 1);
   1.259  qed "if_Suc_diff_n";
   1.260  
   1.261  goal Arith.thy "P(k) --> (!n. P(Suc(n))--> P(n)) --> P(k-i)";
   1.262  by (res_inst_tac [("m","k"),("n","i")] diff_induct 1);
   1.263 -by (ALLGOALS (strip_tac THEN' simp_tac arith_ss THEN' TRY o fast_tac HOL_cs));
   1.264 +by (ALLGOALS (strip_tac THEN' Simp_tac THEN' TRY o fast_tac HOL_cs));
   1.265  qed "zero_induct_lemma";
   1.266  
   1.267  val prems = goal Arith.thy "[| P(k);  !!n. P(Suc(n)) ==> P(n) |] ==> P(0)";
   1.268 @@ -263,13 +261,13 @@
   1.269  
   1.270  goal Arith.thy "!!m. m<n --> (? k. n=Suc(m+k))";
   1.271  by (nat_ind_tac "n" 1);
   1.272 -by (ALLGOALS(simp_tac arith_ss));
   1.273 +by (ALLGOALS(Simp_tac));
   1.274  by (REPEAT_FIRST (ares_tac [conjI, impI]));
   1.275  by (res_inst_tac [("x","0")] exI 2);
   1.276 -by (simp_tac arith_ss 2);
   1.277 +by (Simp_tac 2);
   1.278  by (safe_tac HOL_cs);
   1.279  by (res_inst_tac [("x","Suc(k)")] exI 1);
   1.280 -by (simp_tac arith_ss 1);
   1.281 +by (Simp_tac 1);
   1.282  val less_eq_Suc_add_lemma = result();
   1.283  
   1.284  (*"m<n ==> ? k. n = Suc(m+k)"*)
   1.285 @@ -278,13 +276,13 @@
   1.286  
   1.287  goal Arith.thy "n <= ((m + n)::nat)";
   1.288  by (nat_ind_tac "m" 1);
   1.289 -by (ALLGOALS(simp_tac arith_ss));
   1.290 +by (ALLGOALS Simp_tac);
   1.291  by (etac le_trans 1);
   1.292  by (rtac (lessI RS less_imp_le) 1);
   1.293  qed "le_add2";
   1.294  
   1.295  goal Arith.thy "n <= ((n + m)::nat)";
   1.296 -by (simp_tac (arith_ss addsimps add_ac) 1);
   1.297 +by (simp_tac (!simpset addsimps add_ac) 1);
   1.298  by (rtac le_add2 1);
   1.299  qed "le_add1";
   1.300  
   1.301 @@ -306,7 +304,7 @@
   1.302  goal Arith.thy "!!i. i+j < (k::nat) ==> i<k";
   1.303  be rev_mp 1;
   1.304  by(nat_ind_tac "j" 1);
   1.305 -by (ALLGOALS(asm_simp_tac arith_ss));
   1.306 +by (ALLGOALS Asm_simp_tac);
   1.307  by(fast_tac (HOL_cs addDs [Suc_lessD]) 1);
   1.308  qed "add_lessD1";
   1.309  
   1.310 @@ -322,17 +320,18 @@
   1.311  
   1.312  goal Arith.thy "m+k<=n --> m<=(n::nat)";
   1.313  by (nat_ind_tac "k" 1);
   1.314 -by (ALLGOALS (asm_simp_tac arith_ss));
   1.315 +by (ALLGOALS Asm_simp_tac);
   1.316  by (fast_tac (HOL_cs addDs [Suc_leD]) 1);
   1.317  val add_leD1_lemma = result();
   1.318 -bind_thm ("add_leD1", add_leD1_lemma RS mp);;
   1.319 +bind_thm ("add_leD1", add_leD1_lemma RS mp);
   1.320  
   1.321  goal Arith.thy "!!k l::nat. [| k<l; m+l = k+n |] ==> m<n";
   1.322  by (safe_tac (HOL_cs addSDs [less_eq_Suc_add]));
   1.323  by (asm_full_simp_tac
   1.324 -    (HOL_ss addsimps ([add_Suc_right RS sym, add_left_cancel] @add_ac)) 1);
   1.325 +    (!simpset delsimps [add_Suc_right]
   1.326 +                addsimps ([add_Suc_right RS sym, add_left_cancel] @add_ac)) 1);
   1.327  by (eresolve_tac [subst] 1);
   1.328 -by (simp_tac (arith_ss addsimps [less_add_Suc1]) 1);
   1.329 +by (simp_tac (!simpset addsimps [less_add_Suc1]) 1);
   1.330  qed "less_add_eq_less";
   1.331  
   1.332  
   1.333 @@ -343,7 +342,7 @@
   1.334  (*strict, in 1st argument*)
   1.335  goal Arith.thy "!!i j k::nat. i < j ==> i + k < j + k";
   1.336  by (nat_ind_tac "k" 1);
   1.337 -by (ALLGOALS (asm_simp_tac arith_ss));
   1.338 +by (ALLGOALS Asm_simp_tac);
   1.339  qed "add_less_mono1";
   1.340  
   1.341  (*strict, in both arguments*)
   1.342 @@ -351,7 +350,7 @@
   1.343  by (rtac (add_less_mono1 RS less_trans) 1);
   1.344  by (REPEAT (assume_tac 1));
   1.345  by (nat_ind_tac "j" 1);
   1.346 -by (ALLGOALS (asm_simp_tac arith_ss));
   1.347 +by (ALLGOALS Asm_simp_tac);
   1.348  qed "add_less_mono";
   1.349  
   1.350  (*A [clumsy] way of lifting < monotonicity to <= monotonicity *)
   1.351 @@ -360,7 +359,7 @@
   1.352  \        i <= j					\
   1.353  \     |] ==> f(i) <= (f(j)::nat)";
   1.354  by (cut_facts_tac [le] 1);
   1.355 -by (asm_full_simp_tac (HOL_ss addsimps [le_eq_less_or_eq]) 1);
   1.356 +by (asm_full_simp_tac (!simpset addsimps [le_eq_less_or_eq]) 1);
   1.357  by (fast_tac (HOL_cs addSIs [lt_mono]) 1);
   1.358  qed "less_mono_imp_le_mono";
   1.359  
   1.360 @@ -374,7 +373,7 @@
   1.361  (*non-strict, in both arguments*)
   1.362  goal Arith.thy "!!k l::nat. [|i<=j;  k<=l |] ==> i + k <= j + l";
   1.363  by (etac (add_le_mono1 RS le_trans) 1);
   1.364 -by (simp_tac (HOL_ss addsimps [add_commute]) 1);
   1.365 +by (simp_tac (!simpset addsimps [add_commute]) 1);
   1.366  (*j moves to the end because it is free while k, l are bound*)
   1.367  by (eresolve_tac [add_le_mono1] 1);
   1.368  qed "add_le_mono";
     2.1 --- a/src/HOL/Finite.ML	Wed Oct 04 13:01:05 1995 +0100
     2.2 +++ b/src/HOL/Finite.ML	Wed Oct 04 13:10:03 1995 +0100
     2.3 @@ -33,13 +33,13 @@
     2.4  
     2.5  (** Simplification for Fin **)
     2.6  
     2.7 -val Fin_ss = set_ss addsimps Fin.intrs;
     2.8 +Addsimps Fin.intrs;
     2.9  
    2.10  (*The union of two finite sets is finite*)
    2.11  val major::prems = goal Finite.thy
    2.12      "[| F: Fin(A);  G: Fin(A) |] ==> F Un G : Fin(A)";
    2.13  by (rtac (major RS Fin_induct) 1);
    2.14 -by (ALLGOALS (asm_simp_tac (Fin_ss addsimps (prems@[Un_insert_left]))));
    2.15 +by (ALLGOALS (asm_simp_tac (!simpset addsimps (prems @ [Un_insert_left]))));
    2.16  qed "Fin_UnI";
    2.17  
    2.18  (*Every subset of a finite set is finite*)
    2.19 @@ -48,18 +48,19 @@
    2.20  	    rtac mp, etac spec,
    2.21  	    rtac subs]);
    2.22  by (rtac (fin RS Fin_induct) 1);
    2.23 -by (simp_tac (Fin_ss addsimps [subset_Un_eq]) 1);
    2.24 +by (simp_tac (!simpset addsimps [subset_Un_eq]) 1);
    2.25  by (safe_tac (set_cs addSDs [subset_insert_iff RS iffD1]));
    2.26  by (eres_inst_tac [("t","C")] (insert_Diff RS subst) 2);
    2.27 -by (ALLGOALS (asm_simp_tac Fin_ss));
    2.28 +by (ALLGOALS Asm_simp_tac);
    2.29  qed "Fin_subset";
    2.30  
    2.31  (*The image of a finite set is finite*)
    2.32  val major::_ = goal Finite.thy
    2.33      "F: Fin(A) ==> h``F : Fin(h``A)";
    2.34  by (rtac (major RS Fin_induct) 1);
    2.35 -by (simp_tac Fin_ss 1);
    2.36 -by (asm_simp_tac (set_ss addsimps [image_eqI RS Fin.insertI, image_insert]) 1);
    2.37 +by (Simp_tac 1);
    2.38 +by (asm_simp_tac
    2.39 +    (!simpset addsimps [image_eqI RS Fin.insertI, image_insert]) 1);
    2.40  qed "Fin_imageI";
    2.41  
    2.42  val major::prems = goal Finite.thy 
    2.43 @@ -70,7 +71,7 @@
    2.44  by (rtac (major RS Fin_induct) 1);
    2.45  by (rtac (Diff_insert RS ssubst) 2);
    2.46  by (ALLGOALS (asm_simp_tac
    2.47 -                (Fin_ss addsimps (prems@[Diff_subset RS Fin_subset]))));
    2.48 +                (!simpset addsimps (prems@[Diff_subset RS Fin_subset]))));
    2.49  qed "Fin_empty_induct_lemma";
    2.50  
    2.51  val prems = goal Finite.thy 
     3.1 --- a/src/HOL/Fun.ML	Wed Oct 04 13:01:05 1995 +0100
     3.2 +++ b/src/HOL/Fun.ML	Wed Oct 04 13:10:03 1995 +0100
     3.3 @@ -6,10 +6,12 @@
     3.4  Lemmas about functions.
     3.5  *)
     3.6  
     3.7 +simpset := HOL_ss;
     3.8 +
     3.9  goal Fun.thy "(f = g) = (!x. f(x)=g(x))";
    3.10  by (rtac iffI 1);
    3.11 -by(asm_simp_tac HOL_ss 1);
    3.12 -by(rtac ext 1 THEN asm_simp_tac HOL_ss 1);
    3.13 +by (Asm_simp_tac 1);
    3.14 +by (rtac ext 1 THEN Asm_simp_tac 1);
    3.15  qed "expand_fun_eq";
    3.16  
    3.17  val prems = goal Fun.thy
    3.18 @@ -194,7 +196,6 @@
    3.19  
    3.20  val mksimps_pairs = ("Ball",[bspec]) :: mksimps_pairs;
    3.21  
    3.22 -val set_ss =
    3.23 -  HOL_ss addsimps mem_simps
    3.24 -         addcongs [ball_cong,bex_cong]
    3.25 -         setmksimps (mksimps mksimps_pairs);
    3.26 +simpset := !simpset addsimps mem_simps
    3.27 +                    addcongs [ball_cong,bex_cong]
    3.28 +                    setmksimps (mksimps mksimps_pairs);
     4.1 --- a/src/HOL/Lfp.ML	Wed Oct 04 13:01:05 1995 +0100
     4.2 +++ b/src/HOL/Lfp.ML	Wed Oct 04 13:10:03 1995 +0100
     4.3 @@ -59,7 +59,7 @@
     4.4  brs prems 1;
     4.5  by(res_inst_tac[("p","x")]PairE 1);
     4.6  by(hyp_subst_tac 1);
     4.7 -by(asm_simp_tac (prod_ss addsimps prems) 1);
     4.8 +by(asm_simp_tac (!simpset addsimps prems) 1);
     4.9  qed"induct2";
    4.10  
    4.11  (*** Fixpoint induction a la David Park ***)
     5.1 --- a/src/HOL/Lfp.thy	Wed Oct 04 13:01:05 1995 +0100
     5.2 +++ b/src/HOL/Lfp.thy	Wed Oct 04 13:10:03 1995 +0100
     5.3 @@ -1,4 +1,4 @@
     5.4 -(*  Title: 	HOL/lfp.thy
     5.5 +(*  Title: 	HOL/Lfp.thy
     5.6      ID:         $Id$
     5.7      Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     5.8      Copyright   1992  University of Cambridge
     6.1 --- a/src/HOL/List.ML	Wed Oct 04 13:01:05 1995 +0100
     6.2 +++ b/src/HOL/List.ML	Wed Oct 04 13:10:03 1995 +0100
     6.3 @@ -15,53 +15,39 @@
     6.4  
     6.5  bind_thm("Cons_inject", (hd list.inject) RS iffD1 RS conjE);
     6.6  
     6.7 -val list_ss = HOL_ss addsimps list.simps;
     6.8 -
     6.9  goal List.thy "!x. xs ~= x#xs";
    6.10  by (list.induct_tac "xs" 1);
    6.11 -by (ALLGOALS (asm_simp_tac list_ss));
    6.12 +by (ALLGOALS Asm_simp_tac);
    6.13  qed "not_Cons_self";
    6.14  
    6.15  goal List.thy "(xs ~= []) = (? y ys. xs = y#ys)";
    6.16  by (list.induct_tac "xs" 1);
    6.17 -by (simp_tac list_ss 1);
    6.18 -by (asm_simp_tac list_ss 1);
    6.19 +by (Simp_tac 1);
    6.20 +by (Asm_simp_tac 1);
    6.21  by (REPEAT(resolve_tac [exI,refl,conjI] 1));
    6.22  qed "neq_Nil_conv";
    6.23  
    6.24 -val list_ss = arith_ss addsimps list.simps @
    6.25 -  [null_Nil, null_Cons, hd_Cons, tl_Cons, ttl_Nil, ttl_Cons,
    6.26 -   mem_Nil, mem_Cons,
    6.27 -   append_Nil, append_Cons,
    6.28 -   rev_Nil, rev_Cons,
    6.29 -   map_Nil, map_Cons,
    6.30 -   flat_Nil, flat_Cons,
    6.31 -   list_all_Nil, list_all_Cons,
    6.32 -   filter_Nil, filter_Cons,
    6.33 -   foldl_Nil, foldl_Cons,
    6.34 -   length_Nil, length_Cons];
    6.35 -
    6.36  
    6.37  (** @ - append **)
    6.38  
    6.39  goal List.thy "(xs@ys)@zs = xs@(ys@zs)";
    6.40  by (list.induct_tac "xs" 1);
    6.41 -by (ALLGOALS (asm_simp_tac list_ss));
    6.42 +by (ALLGOALS Asm_simp_tac);
    6.43  qed "append_assoc";
    6.44  
    6.45  goal List.thy "xs @ [] = xs";
    6.46  by (list.induct_tac "xs" 1);
    6.47 -by (ALLGOALS (asm_simp_tac list_ss));
    6.48 +by (ALLGOALS Asm_simp_tac);
    6.49  qed "append_Nil2";
    6.50  
    6.51  goal List.thy "(xs@ys = []) = (xs=[] & ys=[])";
    6.52  by (list.induct_tac "xs" 1);
    6.53 -by (ALLGOALS (asm_simp_tac list_ss));
    6.54 +by (ALLGOALS Asm_simp_tac);
    6.55  qed "append_is_Nil";
    6.56  
    6.57  goal List.thy "(xs @ ys = xs @ zs) = (ys=zs)";
    6.58  by (list.induct_tac "xs" 1);
    6.59 -by (ALLGOALS (asm_simp_tac list_ss));
    6.60 +by (ALLGOALS Asm_simp_tac);
    6.61  qed "same_append_eq";
    6.62  
    6.63  
    6.64 @@ -69,12 +55,12 @@
    6.65  
    6.66  goal List.thy "rev(xs@ys) = rev(ys) @ rev(xs)";
    6.67  by (list.induct_tac "xs" 1);
    6.68 -by (ALLGOALS (asm_simp_tac (list_ss addsimps [append_Nil2,append_assoc])));
    6.69 +by (ALLGOALS (asm_simp_tac (!simpset addsimps [append_Nil2,append_assoc])));
    6.70  qed "rev_append";
    6.71  
    6.72  goal List.thy "rev(rev l) = l";
    6.73  by (list.induct_tac "l" 1);
    6.74 -by (ALLGOALS (asm_simp_tac (list_ss addsimps [rev_append])));
    6.75 +by (ALLGOALS (asm_simp_tac (!simpset addsimps [rev_append])));
    6.76  qed "rev_rev_ident";
    6.77  
    6.78  
    6.79 @@ -82,29 +68,29 @@
    6.80  
    6.81  goal List.thy "x mem (xs@ys) = (x mem xs | x mem ys)";
    6.82  by (list.induct_tac "xs" 1);
    6.83 -by (ALLGOALS (asm_simp_tac (list_ss setloop (split_tac [expand_if]))));
    6.84 +by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
    6.85  qed "mem_append";
    6.86  
    6.87  goal List.thy "x mem [x:xs.P(x)] = (x mem xs & P(x))";
    6.88  by (list.induct_tac "xs" 1);
    6.89 -by (ALLGOALS (asm_simp_tac (list_ss setloop (split_tac [expand_if]))));
    6.90 +by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
    6.91  qed "mem_filter";
    6.92  
    6.93  (** list_all **)
    6.94  
    6.95  goal List.thy "(Alls x:xs.True) = True";
    6.96  by (list.induct_tac "xs" 1);
    6.97 -by (ALLGOALS (asm_simp_tac list_ss));
    6.98 +by (ALLGOALS Asm_simp_tac);
    6.99  qed "list_all_True";
   6.100  
   6.101  goal List.thy "list_all p (xs@ys) = (list_all p xs & list_all p ys)";
   6.102  by (list.induct_tac "xs" 1);
   6.103 -by (ALLGOALS (asm_simp_tac list_ss));
   6.104 +by (ALLGOALS Asm_simp_tac);
   6.105  qed "list_all_conj";
   6.106  
   6.107  goal List.thy "(Alls x:xs.P(x)) = (!x. x mem xs --> P(x))";
   6.108  by (list.induct_tac "xs" 1);
   6.109 -by (ALLGOALS (asm_simp_tac (list_ss setloop (split_tac [expand_if]))));
   6.110 +by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
   6.111  by (fast_tac HOL_cs 1);
   6.112  qed "list_all_mem_conv";
   6.113  
   6.114 @@ -115,7 +101,7 @@
   6.115   "P(list_case a f xs) = ((xs=[] --> P(a)) & \
   6.116  \                         (!y ys. xs=y#ys --> P(f y ys)))";
   6.117  by (list.induct_tac "xs" 1);
   6.118 -by (ALLGOALS (asm_simp_tac list_ss));
   6.119 +by (ALLGOALS Asm_simp_tac);
   6.120  by (fast_tac HOL_cs 1);
   6.121  qed "expand_list_case";
   6.122  
   6.123 @@ -130,19 +116,19 @@
   6.124  
   6.125  goal List.thy  "flat(xs@ys) = flat(xs)@flat(ys)";
   6.126  by (list.induct_tac "xs" 1);
   6.127 -by (ALLGOALS (asm_simp_tac (list_ss addsimps [append_assoc])));
   6.128 +by (ALLGOALS (asm_simp_tac (!simpset addsimps [append_assoc])));
   6.129  qed"flat_append";
   6.130  
   6.131  (** length **)
   6.132  
   6.133  goal List.thy "length(xs@ys) = length(xs)+length(ys)";
   6.134  by (list.induct_tac "xs" 1);
   6.135 -by (ALLGOALS (asm_simp_tac list_ss));
   6.136 +by (ALLGOALS Asm_simp_tac);
   6.137  qed"length_append";
   6.138  
   6.139  goal List.thy "length(rev xs) = length(xs)";
   6.140  by (list.induct_tac "xs" 1);
   6.141 -by (ALLGOALS (asm_simp_tac (list_ss addsimps [length_append])));
   6.142 +by (ALLGOALS (asm_simp_tac (!simpset addsimps [length_append])));
   6.143  qed "length_rev";
   6.144  
   6.145  (** nth **)
   6.146 @@ -156,31 +142,31 @@
   6.147  goal List.thy "map (%x.x) = (%xs.xs)";
   6.148  by (rtac ext 1);
   6.149  by (list.induct_tac "xs" 1);
   6.150 -by (ALLGOALS (asm_simp_tac list_ss));
   6.151 +by (ALLGOALS Asm_simp_tac);
   6.152  qed "map_ident";
   6.153  
   6.154  goal List.thy "map f (xs@ys) = map f xs @ map f ys";
   6.155  by (list.induct_tac "xs" 1);
   6.156 -by (ALLGOALS (asm_simp_tac list_ss));
   6.157 +by (ALLGOALS Asm_simp_tac);
   6.158  qed "map_append";
   6.159  
   6.160  goalw List.thy [o_def] "map (f o g) xs = map f (map g xs)";
   6.161  by (list.induct_tac "xs" 1);
   6.162 -by (ALLGOALS (asm_simp_tac list_ss));
   6.163 +by (ALLGOALS Asm_simp_tac);
   6.164  qed "map_compose";
   6.165  
   6.166  goal List.thy "rev(map f l) = map f (rev l)";
   6.167  by (list.induct_tac "l" 1);
   6.168 -by (ALLGOALS (asm_simp_tac (list_ss addsimps [map_append])));
   6.169 +by (ALLGOALS (asm_simp_tac (!simpset addsimps [map_append])));
   6.170  qed "rev_map_distrib";
   6.171  
   6.172  goal List.thy "rev(flat ls) = flat (map rev (rev ls))";
   6.173  by (list.induct_tac "ls" 1);
   6.174 -by (ALLGOALS (asm_simp_tac (list_ss addsimps 
   6.175 +by (ALLGOALS (asm_simp_tac (!simpset addsimps 
   6.176         [map_append, flat_append, rev_append, append_Nil2])));
   6.177  qed "rev_flat";
   6.178  
   6.179 -val list_ss = list_ss addsimps
   6.180 +Addsimps
   6.181    [not_Cons_self, append_assoc, append_Nil2, append_is_Nil, same_append_eq,
   6.182     mem_append, mem_filter,
   6.183     rev_append, rev_rev_ident,
     7.1 --- a/src/HOL/Makefile	Wed Oct 04 13:01:05 1995 +0100
     7.2 +++ b/src/HOL/Makefile	Wed Oct 04 13:10:03 1995 +0100
     7.3 @@ -88,7 +88,7 @@
     7.4  
     7.5  IOA:    $(BIN)/HOL  $(IOA_FILES)
     7.6  	echo 'exit_use"IOA/ROOT_NTP.ML";quit();' | $(LOGIC)
     7.7 -	echo 'exit_use"IOA/ROOT_ABP.ML";quit();' | $(LOGIC)
     7.8 +#	echo 'exit_use"IOA/ROOT_ABP.ML";quit();' | $(LOGIC)
     7.9  
    7.10  ##Properties of substitutions
    7.11  SUBST_NAMES = AList Setplus Subst Unifier UTerm UTLemmas
    7.12 @@ -118,8 +118,8 @@
    7.13  ex:     $(BIN)/HOL  $(EX_FILES)
    7.14  	echo 'exit_use"ex/ROOT.ML";quit();' | $(LOGIC)
    7.15  
    7.16 -#Full test.
    7.17 -test:   $(BIN)/HOL IMP Integ IOA Subst Lambda ex
    7.18 +#Full test. (IOA has been removed temporarily)
    7.19 +test:   $(BIN)/HOL IMP Integ Subst Lambda ex
    7.20  	echo 'Test examples ran successfully' > test
    7.21  
    7.22  .PRECIOUS:  $(BIN)/Pure $(BIN)/HOL 
     8.1 --- a/src/HOL/Nat.ML	Wed Oct 04 13:01:05 1995 +0100
     8.2 +++ b/src/HOL/Nat.ML	Wed Oct 04 13:10:03 1995 +0100
     8.3 @@ -110,7 +110,7 @@
     8.4  by (etac (inj_Rep_Nat RS injD) 1);
     8.5  qed "inj_Suc";
     8.6  
     8.7 -val Suc_inject = inj_Suc RS injD;;
     8.8 +val Suc_inject = inj_Suc RS injD;
     8.9  
    8.10  goal Nat.thy "(Suc(m)=Suc(n)) = (m=n)";
    8.11  by (EVERY1 [rtac iffI, etac Suc_inject, etac arg_cong]); 
    8.12 @@ -118,7 +118,7 @@
    8.13  
    8.14  goal Nat.thy "n ~= Suc(n)";
    8.15  by (nat_ind_tac "n" 1);
    8.16 -by (ALLGOALS(asm_simp_tac (HOL_ss addsimps [Zero_not_Suc,Suc_Suc_eq])));
    8.17 +by (ALLGOALS(asm_simp_tac (!simpset addsimps [Zero_not_Suc,Suc_Suc_eq])));
    8.18  qed "n_not_Suc_n";
    8.19  
    8.20  val Suc_n_not_n = n_not_Suc_n RS not_sym;
    8.21 @@ -164,12 +164,12 @@
    8.22  
    8.23  goal Nat.thy "nat_rec 0 c h = c";
    8.24  by (rtac (nat_rec_unfold RS trans) 1);
    8.25 -by (simp_tac (HOL_ss addsimps [nat_case_0]) 1);
    8.26 +by (simp_tac (!simpset addsimps [nat_case_0]) 1);
    8.27  qed "nat_rec_0";
    8.28  
    8.29  goal Nat.thy "nat_rec (Suc n) c h = h n (nat_rec n c h)";
    8.30  by (rtac (nat_rec_unfold RS trans) 1);
    8.31 -by (simp_tac (HOL_ss addsimps [nat_case_Suc, pred_natI, cut_apply]) 1);
    8.32 +by (simp_tac (!simpset addsimps [nat_case_Suc, pred_natI, cut_apply]) 1);
    8.33  qed "nat_rec_Suc";
    8.34  
    8.35  (*These 2 rules ease the use of primitive recursion.  NOTE USE OF == *)
    8.36 @@ -328,7 +328,7 @@
    8.37  (*Can be used with less_Suc_eq to get n=m | n<m *)
    8.38  goal Nat.thy "(~ m < n) = (n < Suc(m))";
    8.39  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
    8.40 -by(ALLGOALS(asm_simp_tac (HOL_ss addsimps
    8.41 +by(ALLGOALS(asm_simp_tac (!simpset addsimps
    8.42                            [not_less0,zero_less_Suc,Suc_less_eq])));
    8.43  qed "not_less_eq";
    8.44  
    8.45 @@ -346,13 +346,11 @@
    8.46  by (rtac not_less0 1);
    8.47  qed "le0";
    8.48  
    8.49 -val nat_simps = [not_less0, less_not_refl, zero_less_Suc, lessI, 
    8.50 -		 Suc_less_eq, less_Suc_eq, le0, not_Suc_n_less_n,
    8.51 -		 Suc_not_Zero, Zero_not_Suc, Suc_Suc_eq,
    8.52 -		 n_not_Suc_n, Suc_n_not_n,
    8.53 -		 nat_case_0, nat_case_Suc, nat_rec_0, nat_rec_Suc];
    8.54 -
    8.55 -val nat_ss0 = sum_ss  addsimps  nat_simps;
    8.56 +Addsimps [not_less0, less_not_refl, zero_less_Suc, lessI, 
    8.57 +          Suc_less_eq, less_Suc_eq, le0, not_Suc_n_less_n,
    8.58 +          Suc_not_Zero, Zero_not_Suc, Suc_Suc_eq,
    8.59 +          n_not_Suc_n, Suc_n_not_n,
    8.60 +          nat_case_0, nat_case_Suc, nat_rec_0, nat_rec_Suc];
    8.61  
    8.62  (*Prevents simplification of f and g: much faster*)
    8.63  qed_goal "nat_case_weak_cong" Nat.thy
    8.64 @@ -378,12 +376,12 @@
    8.65  qed "not_leE";
    8.66  
    8.67  goalw Nat.thy [le_def] "!!m. m < n ==> Suc(m) <= n";
    8.68 -by(simp_tac nat_ss0 1);
    8.69 +by(Simp_tac 1);
    8.70  by (fast_tac (HOL_cs addEs [less_anti_refl,less_asym]) 1);
    8.71  qed "lessD";
    8.72  
    8.73  goalw Nat.thy [le_def] "!!m. Suc(m) <= n ==> m <= n";
    8.74 -by(asm_full_simp_tac nat_ss0 1);
    8.75 +by(Asm_full_simp_tac 1);
    8.76  by(fast_tac HOL_cs 1);
    8.77  qed "Suc_leD";
    8.78  
    8.79 @@ -407,7 +405,7 @@
    8.80  qed "le_eq_less_or_eq";
    8.81  
    8.82  goal Nat.thy "n <= (n::nat)";
    8.83 -by(simp_tac (HOL_ss addsimps [le_eq_less_or_eq]) 1);
    8.84 +by(simp_tac (!simpset addsimps [le_eq_less_or_eq]) 1);
    8.85  qed "le_refl";
    8.86  
    8.87  val prems = goal Nat.thy "!!i. [| i <= j; j < k |] ==> i < (k::nat)";
    8.88 @@ -431,7 +429,7 @@
    8.89  qed "le_anti_sym";
    8.90  
    8.91  goal Nat.thy "(Suc(n) <= Suc(m)) = (n <= m)";
    8.92 -by (simp_tac (nat_ss0 addsimps [le_eq_less_or_eq]) 1);
    8.93 +by (simp_tac (!simpset addsimps [le_eq_less_or_eq]) 1);
    8.94  qed "Suc_le_mono";
    8.95  
    8.96 -val nat_ss = nat_ss0 addsimps [le_refl,Suc_le_mono];
    8.97 +Addsimps [le_refl,Suc_le_mono];
     9.1 --- a/src/HOL/Prod.ML	Wed Oct 04 13:01:05 1995 +0100
     9.2 +++ b/src/HOL/Prod.ML	Wed Oct 04 13:10:03 1995 +0100
     9.3 @@ -58,12 +58,12 @@
     9.4  by (rtac refl 1);
     9.5  qed "split";
     9.6  
     9.7 -val prod_ss = set_ss addsimps [fst_conv, snd_conv, split, Pair_eq];
     9.8 +Addsimps [fst_conv, snd_conv, split, Pair_eq];
     9.9  
    9.10  goal Prod.thy "(s=t) = (fst(s)=fst(t) & snd(s)=snd(t))";
    9.11  by (res_inst_tac[("p","s")] PairE 1);
    9.12  by (res_inst_tac[("p","t")] PairE 1);
    9.13 -by (asm_simp_tac prod_ss 1);
    9.14 +by (Asm_simp_tac 1);
    9.15  qed "Pair_fst_snd_eq";
    9.16  
    9.17  (*Prevents simplification of c: much faster*)
    9.18 @@ -74,12 +74,12 @@
    9.19  (* Do not add as rewrite rule: invalidates some proofs in IMP *)
    9.20  goal Prod.thy "p = (fst(p),snd(p))";
    9.21  by (res_inst_tac [("p","p")] PairE 1);
    9.22 -by (asm_simp_tac prod_ss 1);
    9.23 +by (Asm_simp_tac 1);
    9.24  qed "surjective_pairing";
    9.25  
    9.26  goal Prod.thy "p = split (%x y.(x,y)) p";
    9.27  by (res_inst_tac [("p","p")] PairE 1);
    9.28 -by (asm_simp_tac prod_ss 1);
    9.29 +by (Asm_simp_tac 1);
    9.30  qed "surjective_pairing2";
    9.31  
    9.32  (*For use with split_tac and the simplifier*)
    9.33 @@ -95,7 +95,7 @@
    9.34    Could instead call simp_tac/asm_full_simp_tac using split as rewrite.*)
    9.35  
    9.36  goal Prod.thy "!!a b c. c a b ==> split c (a,b)";
    9.37 -by (asm_simp_tac prod_ss 1);
    9.38 +by (Asm_simp_tac 1);
    9.39  qed "splitI";
    9.40  
    9.41  val prems = goalw Prod.thy [split_def]
    9.42 @@ -108,7 +108,7 @@
    9.43  qed "splitD";
    9.44  
    9.45  goal Prod.thy "!!a b c. z: c a b ==> z: split c (a,b)";
    9.46 -by (asm_simp_tac prod_ss 1);
    9.47 +by (Asm_simp_tac 1);
    9.48  qed "mem_splitI";
    9.49  
    9.50  val prems = goalw Prod.thy [split_def]
    9.51 @@ -126,13 +126,13 @@
    9.52      "prod_fun (f1 o f2) (g1 o g2) = ((prod_fun f1 g1) o (prod_fun f2 g2))";
    9.53  by (rtac ext 1);
    9.54  by (res_inst_tac [("p","x")] PairE 1);
    9.55 -by (asm_simp_tac (prod_ss addsimps [prod_fun,o_def]) 1);
    9.56 +by (asm_simp_tac (!simpset addsimps [prod_fun,o_def]) 1);
    9.57  qed "prod_fun_compose";
    9.58  
    9.59  goal Prod.thy "prod_fun (%x.x) (%y.y) = (%z.z)";
    9.60  by (rtac ext 1);
    9.61  by (res_inst_tac [("p","z")] PairE 1);
    9.62 -by (asm_simp_tac (prod_ss addsimps [prod_fun]) 1);
    9.63 +by (asm_simp_tac (!simpset addsimps [prod_fun]) 1);
    9.64  qed "prod_fun_ident";
    9.65  
    9.66  val prems = goal Prod.thy "(a,b):r ==> (f(a),g(b)) : (prod_fun f g)``r";
    10.1 --- a/src/HOL/ROOT.ML	Wed Oct 04 13:01:05 1995 +0100
    10.2 +++ b/src/HOL/ROOT.ML	Wed Oct 04 13:10:03 1995 +0100
    10.3 @@ -1,4 +1,4 @@
    10.4 -(*  Title:      CHOL/ROOT.ML
    10.5 +(*  Title:      HOL/ROOT.ML
    10.6      ID:         $Id$
    10.7      Author:     Tobias Nipkow
    10.8      Copyright   1993  University of Cambridge
    10.9 @@ -18,7 +18,6 @@
   10.10  use "thy_syntax.ML";
   10.11  
   10.12  use_thy "HOL";
   10.13 -use "../Provers/simplifier.ML";
   10.14  use "../Provers/splitter.ML";
   10.15  use "../Provers/hypsubst.ML";
   10.16  use "../Provers/classical.ML";
   10.17 @@ -64,7 +63,6 @@
   10.18  use     "simpdata.ML";
   10.19  use_thy "Ord";
   10.20  use_thy "subset";
   10.21 -use_thy "equalities";
   10.22  use     "hologic.ML";
   10.23  use     "subtype.ML";
   10.24  use_thy "Prod";
    11.1 --- a/src/HOL/Relation.ML	Wed Oct 04 13:01:05 1995 +0100
    11.2 +++ b/src/HOL/Relation.ML	Wed Oct 04 13:10:03 1995 +0100
    11.3 @@ -83,7 +83,7 @@
    11.4  (** Natural deduction for converse(r) **)
    11.5  
    11.6  goalw Relation.thy [converse_def] "!!a b r. (a,b):r ==> (b,a):converse(r)";
    11.7 -by (simp_tac prod_ss 1);
    11.8 +by (Simp_tac 1);
    11.9  by (fast_tac set_cs 1);
   11.10  qed "converseI";
   11.11  
   11.12 @@ -170,4 +170,4 @@
   11.13  
   11.14  val rel_eq_cs = rel_cs addSIs [equalityI];
   11.15  
   11.16 -val rel_ss = prod_ss addsimps [pair_in_id_conv];
   11.17 +Addsimps [pair_in_id_conv];
    12.1 --- a/src/HOL/Sexp.ML	Wed Oct 04 13:01:05 1995 +0100
    12.2 +++ b/src/HOL/Sexp.ML	Wed Oct 04 13:10:03 1995 +0100
    12.3 @@ -87,11 +87,8 @@
    12.4  and pred_sexp_trans2 = pred_sexp_t2 RSN (2, trans_trancl RS transD);
    12.5  
    12.6  (*Proves goals of the form (M,N):pred_sexp^+ provided M,N:sexp*)
    12.7 -val pred_sexp_simps =
    12.8 -            sexp.intrs @
    12.9 -	    [pred_sexp_t1, pred_sexp_t2,
   12.10 -	     pred_sexp_trans1, pred_sexp_trans2, cut_apply];
   12.11 -val pred_sexp_ss = HOL_ss addsimps pred_sexp_simps;
   12.12 +Addsimps (sexp.intrs @ [pred_sexp_t1, pred_sexp_t2,
   12.13 +	                pred_sexp_trans1, pred_sexp_trans2, cut_apply]);
   12.14  
   12.15  val major::prems = goalw Sexp.thy [pred_sexp_def]
   12.16      "[| p : pred_sexp;  \
   12.17 @@ -130,6 +127,6 @@
   12.18  goal Sexp.thy "!!M. [| M: sexp;  N: sexp |] ==> \
   12.19  \    sexp_rec (M$N) c d h = h M N (sexp_rec M c d h) (sexp_rec N c d h)";
   12.20  by (rtac (sexp_rec_unfold RS trans) 1);
   12.21 -by (asm_simp_tac(HOL_ss addsimps
   12.22 -               [sexp_case_Scons,pred_sexpI1,pred_sexpI2,cut_apply])1);
   12.23 +by (asm_simp_tac (!simpset addsimps [sexp_case_Scons,pred_sexpI1,pred_sexpI2])
   12.24 +    1);
   12.25  qed "sexp_rec_Scons";
    13.1 --- a/src/HOL/Sum.ML	Wed Oct 04 13:01:05 1995 +0100
    13.2 +++ b/src/HOL/Sum.ML	Wed Oct 04 13:10:03 1995 +0100
    13.3 @@ -44,11 +44,11 @@
    13.4  val Inr_neq_Inl = sym RS Inl_neq_Inr;
    13.5  
    13.6  goal Sum.thy "(Inl(a)=Inr(b)) = False";
    13.7 -by (simp_tac (HOL_ss addsimps [Inl_not_Inr]) 1);
    13.8 +by (simp_tac (!simpset addsimps [Inl_not_Inr]) 1);
    13.9  qed "Inl_Inr_eq";
   13.10  
   13.11  goal Sum.thy "(Inr(b)=Inl(a))  =  False";
   13.12 -by (simp_tac (HOL_ss addsimps [Inl_not_Inr RS not_sym]) 1);
   13.13 +by (simp_tac (!simpset addsimps [Inl_not_Inr RS not_sym]) 1);
   13.14  qed "Inr_Inl_eq";
   13.15  
   13.16  
   13.17 @@ -157,8 +157,7 @@
   13.18  by (fast_tac (set_cs addSEs [make_elim Inr_inject, Inr_neq_Inl]) 1);
   13.19  qed "expand_sum_case";
   13.20  
   13.21 -val sum_ss = prod_ss addsimps [Inl_eq, Inr_eq, Inl_Inr_eq, Inr_Inl_eq, 
   13.22 -			       sum_case_Inl, sum_case_Inr];
   13.23 +Addsimps [Inl_eq, Inr_eq, Inl_Inr_eq, Inr_Inl_eq,  sum_case_Inl, sum_case_Inr];
   13.24  
   13.25  (*Prevents simplification of f and g: much faster*)
   13.26  qed_goal "sum_case_weak_cong" Sum.thy
    14.1 --- a/src/HOL/Univ.ML	Wed Oct 04 13:01:05 1995 +0100
    14.2 +++ b/src/HOL/Univ.ML	Wed Oct 04 13:10:03 1995 +0100
    14.3 @@ -242,7 +242,7 @@
    14.4  (** Leaf vs Numb **)
    14.5  
    14.6  goalw Univ.thy [Leaf_def,Numb_def] "Leaf(a) ~= Numb(k)";
    14.7 -by (simp_tac (HOL_ss addsimps [Atom_Atom_eq,Inl_not_Inr]) 1);
    14.8 +by (simp_tac (!simpset addsimps [Atom_Atom_eq,Inl_not_Inr]) 1);
    14.9  qed "Leaf_not_Numb";
   14.10  bind_thm ("Numb_not_Leaf", (Leaf_not_Numb RS not_sym));
   14.11  
   14.12 @@ -252,8 +252,7 @@
   14.13  
   14.14  (*** ndepth -- the depth of a node ***)
   14.15  
   14.16 -val univ_simps = [apfst_conv,Scons_not_Atom,Atom_not_Scons,Scons_Scons_eq];
   14.17 -val univ_ss = nat_ss addsimps univ_simps;
   14.18 +Addsimps [apfst_conv,Scons_not_Atom,Atom_not_Scons,Scons_Scons_eq];
   14.19  
   14.20  
   14.21  goalw Univ.thy [ndepth_def] "ndepth (Abs_Node((%k.0, x))) = 0";
   14.22 @@ -265,7 +264,7 @@
   14.23  
   14.24  goal Univ.thy "k < Suc(LEAST x. f(x)=0) --> nat_case (Suc i) f k ~= 0";
   14.25  by (nat_ind_tac "k" 1);
   14.26 -by (ALLGOALS (simp_tac nat_ss));
   14.27 +by (ALLGOALS Simp_tac);
   14.28  by (rtac impI 1);
   14.29  by (etac not_less_Least 1);
   14.30  qed "ndepth_Push_lemma";
   14.31 @@ -276,7 +275,7 @@
   14.32  by (cut_facts_tac [rewrite_rule [Node_def] Rep_Node] 1);
   14.33  by (safe_tac set_cs);
   14.34  be ssubst 1;  (*instantiates type variables!*)
   14.35 -by (simp_tac univ_ss 1);
   14.36 +by (Simp_tac 1);
   14.37  by (rtac Least_equality 1);
   14.38  by (rewtac Push_def);
   14.39  by (rtac (nat_case_Suc RS trans) 1);
   14.40 @@ -317,25 +316,25 @@
   14.41  (** Injection nodes **)
   14.42  
   14.43  goalw Univ.thy [In0_def] "ntrunc (Suc 0) (In0 M) = {}";
   14.44 -by (simp_tac (univ_ss addsimps [ntrunc_Scons,ntrunc_0]) 1);
   14.45 +by (simp_tac (!simpset addsimps [ntrunc_Scons,ntrunc_0]) 1);
   14.46  by (rewtac Scons_def);
   14.47  by (safe_tac (set_cs addSIs [equalityI]));
   14.48  qed "ntrunc_one_In0";
   14.49  
   14.50  goalw Univ.thy [In0_def]
   14.51      "ntrunc (Suc (Suc k)) (In0 M) = In0 (ntrunc (Suc k) M)";
   14.52 -by (simp_tac (univ_ss addsimps [ntrunc_Scons,ntrunc_Numb]) 1);
   14.53 +by (simp_tac (!simpset addsimps [ntrunc_Scons,ntrunc_Numb]) 1);
   14.54  qed "ntrunc_In0";
   14.55  
   14.56  goalw Univ.thy [In1_def] "ntrunc (Suc 0) (In1 M) = {}";
   14.57 -by (simp_tac (univ_ss addsimps [ntrunc_Scons,ntrunc_0]) 1);
   14.58 +by (simp_tac (!simpset addsimps [ntrunc_Scons,ntrunc_0]) 1);
   14.59  by (rewtac Scons_def);
   14.60  by (safe_tac (set_cs addSIs [equalityI]));
   14.61  qed "ntrunc_one_In1";
   14.62  
   14.63  goalw Univ.thy [In1_def]
   14.64      "ntrunc (Suc (Suc k)) (In1 M) = In1 (ntrunc (Suc k) M)";
   14.65 -by (simp_tac (univ_ss addsimps [ntrunc_Scons,ntrunc_Numb]) 1);
   14.66 +by (simp_tac (!simpset addsimps [ntrunc_Scons,ntrunc_Numb]) 1);
   14.67  qed "ntrunc_In1";
   14.68  
   14.69  
   14.70 @@ -611,5 +610,4 @@
   14.71                       addSEs [usumE, dsumE]) 1);
   14.72  qed "fst_image_dsum";
   14.73  
   14.74 -val fst_image_simps = [fst_image_diag, fst_image_dprod, fst_image_dsum];
   14.75 -val fst_image_ss = univ_ss addsimps fst_image_simps;
   14.76 +Addsimps [fst_image_diag, fst_image_dprod, fst_image_dsum];
    15.1 --- a/src/HOL/WF.ML	Wed Oct 04 13:01:05 1995 +0100
    15.2 +++ b/src/HOL/WF.ML	Wed Oct 04 13:10:03 1995 +0100
    15.3 @@ -69,12 +69,12 @@
    15.4    H_cong to expose the equality*)
    15.5  goalw WF.thy [cut_def]
    15.6      "(cut f r x = cut g r x) = (!y. (y,x):r --> f(y)=g(y))";
    15.7 -by(simp_tac (HOL_ss addsimps [expand_fun_eq]
    15.8 -                    setloop (split_tac [expand_if])) 1);
    15.9 +by(simp_tac (!simpset addsimps [expand_fun_eq]
   15.10 +                        setloop (split_tac [expand_if])) 1);
   15.11  qed "cut_cut_eq";
   15.12  
   15.13  goalw WF.thy [cut_def] "!!x. (x,a):r ==> (cut f r a)(x) = f(x)";
   15.14 -by(asm_simp_tac HOL_ss 1);
   15.15 +by(Asm_simp_tac 1);
   15.16  qed "cut_apply";
   15.17  
   15.18  
   15.19 @@ -83,7 +83,7 @@
   15.20  goalw WF.thy [is_recfun_def,cut_def]
   15.21      "!!f. [| is_recfun r a H f;  ~(b,a):r |] ==> f(b) = (@z.True)";
   15.22  by (etac ssubst 1);
   15.23 -by(asm_simp_tac HOL_ss 1);
   15.24 +by(Asm_simp_tac 1);
   15.25  qed "is_recfun_undef";
   15.26  
   15.27  (*eresolve_tac transD solves (a,b):r using transitivity AT MOST ONCE
   15.28 @@ -100,7 +100,7 @@
   15.29      (cut_facts_tac hyps THEN'
   15.30         DEPTH_SOLVE_1 o (ares_tac [TrueI] ORELSE'
   15.31  		        eresolve_tac [transD, mp, allE]));
   15.32 -val wf_super_ss = HOL_ss setsolver indhyp_tac;
   15.33 +val wf_super_ss = !simpset setsolver indhyp_tac;
   15.34  
   15.35  val prems = goalw WF.thy [is_recfun_def,cut_def]
   15.36      "[| wf(r);  trans(r);  is_recfun r a H f;  is_recfun r b H g |] ==> \
   15.37 @@ -168,7 +168,7 @@
   15.38  \    wftrec r a H = H a (cut (%x.wftrec r x H) r a)";
   15.39  by (EVERY1 [stac (rewrite_rule [is_recfun_def] unfold_the_recfun),
   15.40  	    REPEAT o atac, rtac H_cong1]);
   15.41 -by (asm_simp_tac (HOL_ss addsimps [cut_cut_eq,the_recfun_cut]) 1);
   15.42 +by (asm_simp_tac (!simpset addsimps [cut_cut_eq,the_recfun_cut]) 1);
   15.43  qed "wftrec";
   15.44  
   15.45  (*Unused but perhaps interesting*)
   15.46 @@ -186,7 +186,7 @@
   15.47  by (etac (wf_trancl RS wftrec RS ssubst) 1);
   15.48  by (rtac trans_trancl 1);
   15.49  by (rtac (refl RS H_cong) 1);    (*expose the equality of cuts*)
   15.50 -by (simp_tac (HOL_ss addsimps [cut_cut_eq, cut_apply, r_into_trancl]) 1);
   15.51 +by (simp_tac (!simpset addsimps [cut_cut_eq, cut_apply, r_into_trancl]) 1);
   15.52  qed "wfrec";
   15.53  
   15.54  (*This form avoids giant explosions in proofs.  NOTE USE OF == *)
    16.1 --- a/src/HOL/equalities.ML	Wed Oct 04 13:01:05 1995 +0100
    16.2 +++ b/src/HOL/equalities.ML	Wed Oct 04 13:10:03 1995 +0100
    16.3 @@ -337,7 +337,7 @@
    16.4  by (fast_tac eq_cs 1);
    16.5  qed "Diff_Int";
    16.6  
    16.7 -val set_ss = set_ss addsimps
    16.8 +Addsimps
    16.9    [in_empty,in_insert,insert_subset,
   16.10     insert_not_empty,empty_not_insert,
   16.11     Int_absorb,Int_empty_left,Int_empty_right,
    17.1 --- a/src/HOL/indrule.ML	Wed Oct 04 13:01:05 1995 +0100
    17.2 +++ b/src/HOL/indrule.ML	Wed Oct 04 13:10:03 1995 +0100
    17.3 @@ -87,7 +87,7 @@
    17.4        (fn prems =>
    17.5         [rtac (impI RS allI) 1,
    17.6  	DETERM (etac raw_induct 1),
    17.7 -	asm_full_simp_tac (HOL_ss addsimps [Part_Collect]) 1,
    17.8 +	asm_full_simp_tac (!simpset addsimps [Part_Collect]) 1,
    17.9  	REPEAT (FIRSTGOAL (eresolve_tac [IntE, CollectE, exE, conjE, disjE] 
   17.10  			   ORELSE' hyp_subst_tac)),
   17.11  	ind_tac (rev prems) (length prems)])
   17.12 @@ -141,7 +141,8 @@
   17.13  
   17.14  (*Simplification largely reduces the mutual induction rule to the 
   17.15    standard rule*)
   17.16 -val mut_ss = set_ss addsimps [Inl_Inr_eq, Inr_Inl_eq, Inl_eq, Inr_eq];
   17.17 +val mut_ss = simpset_of "Fun"
   17.18 +             addsimps [Inl_Inr_eq, Inr_Inl_eq, Inl_eq, Inr_eq];
   17.19  
   17.20  val all_defs = con_defs@part_rec_defs;
   17.21  
    18.1 --- a/src/HOL/intr_elim.ML	Wed Oct 04 13:01:05 1995 +0100
    18.2 +++ b/src/HOL/intr_elim.ML	Wed Oct 04 13:10:03 1995 +0100
    18.3 @@ -126,7 +126,7 @@
    18.4  fun con_elim_tac simps =
    18.5    let val elim_tac = REPEAT o (eresolve_tac (elim_rls@sumprod_free_SEs))
    18.6    in ALLGOALS(EVERY'[elim_tac,
    18.7 -                     asm_full_simp_tac (nat_ss addsimps simps),
    18.8 +                     asm_full_simp_tac (simpset_of "Nat" addsimps simps),
    18.9                       elim_tac,
   18.10                       REPEAT o bound_hyp_subst_tac])
   18.11       THEN prune_params_tac
    19.1 --- a/src/HOL/mono.ML	Wed Oct 04 13:01:05 1995 +0100
    19.2 +++ b/src/HOL/mono.ML	Wed Oct 04 13:10:03 1995 +0100
    19.3 @@ -1,4 +1,4 @@
    19.4 -(*  Title: 	HOL/mono
    19.5 +(*  Title: 	HOL/mono.ML
    19.6      ID:         $Id$
    19.7      Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    19.8      Copyright   1991  University of Cambridge
    20.1 --- a/src/HOL/mono.thy	Wed Oct 04 13:01:05 1995 +0100
    20.2 +++ b/src/HOL/mono.thy	Wed Oct 04 13:10:03 1995 +0100
    20.3 @@ -1,8 +1,8 @@
    20.4 -(*  Title: 	HOL/mono
    20.5 +(*  Title: 	HOL/mono.thy
    20.6      ID:         $Id$
    20.7      Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    20.8      Copyright   1991  University of Cambridge
    20.9  
   20.10  *)
   20.11  
   20.12 -mono = subset
   20.13 +mono = equalities
    21.1 --- a/src/HOL/simpdata.ML	Wed Oct 04 13:01:05 1995 +0100
    21.2 +++ b/src/HOL/simpdata.ML	Wed Oct 04 13:10:03 1995 +0100
    21.3 @@ -98,6 +98,8 @@
    21.4  infix 4 addcongs;
    21.5  fun ss addcongs congs = ss addeqcongs (congs RL [eq_reflection]);
    21.6  
    21.7 +fun Addcongs congs = (simpset := !simpset addcongs congs);
    21.8 +
    21.9  (*Add a simpset to a classical set!*)
   21.10  infix 4 addss;
   21.11  fun cs addss ss = cs addbefore asm_full_simp_tac ss 1;
    22.1 --- a/src/HOL/subtype.ML	Wed Oct 04 13:01:05 1995 +0100
    22.2 +++ b/src/HOL/subtype.ML	Wed Oct 04 13:10:03 1995 +0100
    22.3 @@ -45,7 +45,7 @@
    22.4  
    22.5  fun ext_subtype prep_term name (t, vs, mx) raw_set axms thms usr_tac thy =
    22.6    let
    22.7 -    val _ = require_thy thy "Set" "subtype definitions";
    22.8 +    val dummy = require_thy thy "Set" "subtype definitions";
    22.9      val sign = sign_of thy;
   22.10  
   22.11      (*rhs*)
    23.1 --- a/src/HOL/thy_syntax.ML	Wed Oct 04 13:01:05 1995 +0100
    23.2 +++ b/src/HOL/thy_syntax.ML	Wed Oct 04 13:10:03 1995 +0100
    23.3 @@ -134,7 +134,8 @@
    23.4      \ val recs =" ^ mk_rules tname cons "_rec_" ^ ";\n\
    23.5      \ val simps = inject @ distinct @ cases @ recs;\n\
    23.6      \ fun induct_tac a = res_inst_tac [(" ^ quote tname ^ ", a)] induct;\n\
    23.7 -    \end;\n");
    23.8 +    \end;\n\
    23.9 +    \val dummy = Addsimps " ^ tname ^ ".simps;\n");
   23.10  
   23.11    (*parsers*)
   23.12    val tvars = type_args >> map (cat "dtVar");
   23.13 @@ -159,11 +160,14 @@
   23.14  fun mk_primrec_decl ((fname, tname), axms) =
   23.15    let
   23.16      fun mk_prove (name, eqn) =
   23.17 -      "val " ^ name ^ " = store_thm (" ^ quote name ^ ", prove_goalw thy [get_def thy " 
   23.18 -      ^ fname ^ "] " ^ eqn ^ "\n\
   23.19 -      \  (fn _ => [simp_tac (HOL_ss addsimps " ^ tname ^ ".recs) 1]));";
   23.20 +      "val " ^ name ^ " = store_thm (" ^ quote name
   23.21 +      ^ ", prove_goalw thy [get_def thy " ^ fname ^ "] " ^ eqn ^ "\n\
   23.22 +      \  (fn _ => [Simp_tac 1]));";
   23.23 +
   23.24      val axs = mk_list (map (fn (n, a) => mk_pair (quote n, a)) axms);
   23.25 -  in ("|> " ^ tname ^ "_add_primrec " ^ axs, cat_lines (map mk_prove axms)) end;
   23.26 +  in ("|> " ^ tname ^ "_add_primrec " ^ axs, cat_lines (map mk_prove axms)
   23.27 +      ^ "\nval dummy = Addsimps " ^ mk_list (map fst axms) ^ ";")
   23.28 +  end;
   23.29  
   23.30  val primrec_decl =
   23.31    name -- long_id -- repeat1 (ident -- string) >> mk_primrec_decl;
    24.1 --- a/src/HOL/typedef.ML	Wed Oct 04 13:01:05 1995 +0100
    24.2 +++ b/src/HOL/typedef.ML	Wed Oct 04 13:10:03 1995 +0100
    24.3 @@ -45,7 +45,7 @@
    24.4  
    24.5  fun ext_subtype prep_term name (t, vs, mx) raw_set axms thms usr_tac thy =
    24.6    let
    24.7 -    val _ = require_thy thy "Set" "subtype definitions";
    24.8 +    val dummy = require_thy thy "Set" "subtype definitions";
    24.9      val sign = sign_of thy;
   24.10  
   24.11      (*rhs*)