# HG changeset patch # User paulson # Date 906725216 -7200 # Node ID 8c7e1190e789cb36e493eee8321d03ac38f05e5e # Parent 0067dd151d7a9defc67bc37a8a71f4411da7ccc7 Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants diff -r 0067dd151d7a -r 8c7e1190e789 src/HOL/UNITY/SubstAx.ML --- 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}) \ diff -r 0067dd151d7a -r 8c7e1190e789 src/HOL/ex/BinEx.ML --- 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";