--- a/src/HOL/Integ/Bin.ML Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/Integ/Bin.ML Sat Mar 07 16:29:29 1998 +0100
@@ -100,8 +100,6 @@
(**** The carry/borrow functions, bin_succ and bin_pred ****)
-val if_ss = simpset() addsplits [expand_if];
-
(**** integ_of_bin ****)
@@ -109,26 +107,26 @@
qed_goal "integ_of_bin_norm_Bcons" Bin.thy
"integ_of_bin(norm_Bcons w b) = integ_of_bin(Bcons w b)"
(fn _ =>[(bin.induct_tac "w" 1),
- (ALLGOALS(simp_tac if_ss)) ]);
+ (ALLGOALS Simp_tac) ]);
qed_goal "integ_of_bin_succ" Bin.thy
"integ_of_bin(bin_succ w) = $#1 + integ_of_bin w"
(fn _ =>[(rtac bin.induct 1),
(ALLGOALS(asm_simp_tac
- (if_ss addsimps (integ_of_bin_norm_Bcons::zadd_ac)))) ]);
+ (simpset() addsimps (integ_of_bin_norm_Bcons::zadd_ac)))) ]);
qed_goal "integ_of_bin_pred" Bin.thy
"integ_of_bin(bin_pred w) = $~ ($#1) + integ_of_bin w"
(fn _ =>[(rtac bin.induct 1),
(ALLGOALS(asm_simp_tac
- (if_ss addsimps (integ_of_bin_norm_Bcons::zadd_ac)))) ]);
+ (simpset() addsimps (integ_of_bin_norm_Bcons::zadd_ac)))) ]);
qed_goal "integ_of_bin_minus" Bin.thy
"integ_of_bin(bin_minus w) = $~ (integ_of_bin w)"
(fn _ =>[(rtac bin.induct 1),
(Simp_tac 1),
(Simp_tac 1),
- (asm_simp_tac (if_ss
+ (asm_simp_tac (simpset()
delsimps [pred_Plus,pred_Minus,pred_Bcons]
addsimps [integ_of_bin_succ,integ_of_bin_pred,
zadd_assoc]) 1)]);
@@ -143,16 +141,16 @@
goal Bin.thy
"! w. integ_of_bin(bin_add v w) = integ_of_bin v + integ_of_bin w";
by (bin.induct_tac "v" 1);
-by (simp_tac (if_ss addsimps bin_add_simps) 1);
-by (simp_tac (if_ss addsimps bin_add_simps) 1);
+by (simp_tac (simpset() addsimps bin_add_simps) 1);
+by (simp_tac (simpset() addsimps bin_add_simps) 1);
by (rtac allI 1);
by (bin.induct_tac "w" 1);
-by (asm_simp_tac (if_ss addsimps (bin_add_simps)) 1);
-by (asm_simp_tac (if_ss addsimps (bin_add_simps @ zadd_ac)) 1);
+by (asm_simp_tac (simpset() addsimps (bin_add_simps)) 1);
+by (asm_simp_tac (simpset() addsimps (bin_add_simps @ zadd_ac)) 1);
by (cut_inst_tac [("P","bool")] True_or_False 1);
by (etac disjE 1);
-by (asm_simp_tac (if_ss addsimps (bin_add_simps @ zadd_ac)) 1);
-by (asm_simp_tac (if_ss addsimps (bin_add_simps @ zadd_ac)) 1);
+by (asm_simp_tac (simpset() addsimps (bin_add_simps @ zadd_ac)) 1);
+by (asm_simp_tac (simpset() addsimps (bin_add_simps @ zadd_ac)) 1);
val integ_of_bin_add_lemma = result();
goal Bin.thy "integ_of_bin(bin_add v w) = integ_of_bin v + integ_of_bin w";
@@ -165,12 +163,12 @@
goal Bin.thy "integ_of_bin(bin_mult v w) = integ_of_bin v * integ_of_bin w";
by (bin.induct_tac "v" 1);
-by (simp_tac (if_ss addsimps bin_mult_simps) 1);
-by (simp_tac (if_ss addsimps bin_mult_simps) 1);
+by (simp_tac (simpset() addsimps bin_mult_simps) 1);
+by (simp_tac (simpset() addsimps bin_mult_simps) 1);
by (cut_inst_tac [("P","bool")] True_or_False 1);
by (etac disjE 1);
-by (asm_simp_tac (if_ss addsimps (bin_mult_simps @ [zadd_zmult_distrib])) 2);
-by (asm_simp_tac (if_ss addsimps (bin_mult_simps @ [zadd_zmult_distrib] @
+by (asm_simp_tac (simpset() addsimps (bin_mult_simps @ [zadd_zmult_distrib])) 2);
+by (asm_simp_tac (simpset() addsimps (bin_mult_simps @ [zadd_zmult_distrib] @
zadd_ac)) 1);
qed "integ_of_bin_mult";