--- a/src/HOL/UNITY/SubstAx.ML Fri Sep 25 14:06:27 1998 +0200
+++ b/src/HOL/UNITY/SubstAx.ML Fri Sep 25 14:06:56 1998 +0200
@@ -356,11 +356,11 @@
\ ((A Int {s. f s < z}) Un B); \
\ id: Acts prg |] \
\ ==> LeadsTo prg A B";
-by (res_inst_tac [("f", "nat_of o f")] (allI RS LessThan_induct) 1);
+by (res_inst_tac [("f", "nat o f")] (allI RS LessThan_induct) 1);
by (simp_tac (simpset() addsimps [vimage_def]) 1);
br ([reach, prem] MRS reachable_LeadsTo_weaken) 1;
by (auto_tac (claset(),
- simpset() addsimps [id, nat_of_eq_iff, nat_of_less_iff]));
+ simpset() addsimps [id, nat_eq_iff, nat_less_iff]));
qed "integ_0_le_induct";
Goal "[| ALL m:(greaterThan l). LeadsTo prg (A Int f-``{m}) \
--- a/src/HOL/ex/BinEx.ML Fri Sep 25 14:06:27 1998 +0200
+++ b/src/HOL/ex/BinEx.ML Fri Sep 25 14:06:56 1998 +0200
@@ -140,8 +140,6 @@
by (ALLGOALS Asm_simp_tac);
qed_spec_mp "bin_add_normal";
-
-
Goal "w: normal ==> (w = Pls) = (integ_of w = #0)";
by (etac normal.induct 1);
by Auto_tac;
@@ -154,15 +152,14 @@
by (assume_tac 1);
by (asm_full_simp_tac (simpset() addsimps [normal_Pls_eq_0]) 1);
by (asm_full_simp_tac
- (simpset_of Integ.thy addsimps [integ_of_minus, iszero_def,
- zminus_exchange]) 1);
+ (simpset_of Int.thy addsimps [integ_of_minus, iszero_def,
+ zminus_exchange]) 1);
qed "bin_minus_normal";
-
Goal "w : normal ==> z: normal --> bin_mult w z : normal";
by (etac normal.induct 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [bin_minus_normal,
- bin_mult_BIT])));
+by (ALLGOALS
+ (asm_simp_tac (simpset() addsimps [bin_minus_normal, bin_mult_BIT])));
by (safe_tac (claset() addSDs [normal_BIT_D]));
by (asm_simp_tac (simpset() addsimps [bin_add_normal]) 1);
qed_spec_mp "bin_mult_normal";