# 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";