--- a/src/HOL/Real/Hyperreal/Filter.ML Wed May 10 21:04:16 2000 +0200
+++ b/src/HOL/Real/Hyperreal/Filter.ML Wed May 10 22:34:30 2000 +0200
@@ -552,5 +552,3 @@
val FreeUltrafilter_Ex = export FreeUltrafilter_ex;
Close_locale "UFT";
-
-
--- a/src/HOL/Real/Hyperreal/HyperDef.ML Wed May 10 21:04:16 2000 +0200
+++ b/src/HOL/Real/Hyperreal/HyperDef.ML Wed May 10 22:34:30 2000 +0200
@@ -1857,371 +1857,3 @@
"hypreal_of_nat n = hypreal_of_real (real_of_nat n)";
by (simp_tac (simpset() addsimps [hypreal_add,hypreal_minus]) 1);
qed "hypreal_of_nat_real_of_nat";
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
--- a/src/HOL/Real/Hyperreal/Zorn.ML Wed May 10 21:04:16 2000 +0200
+++ b/src/HOL/Real/Hyperreal/Zorn.ML Wed May 10 22:34:30 2000 +0200
@@ -289,4 +289,3 @@
Goal "x : Union(c) ==> EX m:c. x:m";
by (Blast_tac 1);
qed "mem_UnionD";
-
--- a/src/HOL/Real/PNat.ML Wed May 10 21:04:16 2000 +0200
+++ b/src/HOL/Real/PNat.ML Wed May 10 22:34:30 2000 +0200
@@ -226,7 +226,8 @@
by (auto_tac (claset() addDs [(inj_on_Abs_pnat RS inj_onD)]
addSDs [add_eq_self_zero],
simpset() addsimps [sum_Rep_pnat, Rep_pnat,Abs_pnat_inverse,
- Rep_pnat_gt_zero RS less_not_refl2]));
+ Rep_pnat_gt_zero RS less_not_refl2]
+ delsimprocs Nat_Numeral_Simprocs.cancel_numerals));
qed "pnat_no_add_ident";
--- a/src/HOL/Real/PNat.thy Wed May 10 21:04:16 2000 +0200
+++ b/src/HOL/Real/PNat.thy Wed May 10 22:34:30 2000 +0200
@@ -6,7 +6,7 @@
*)
-PNat = Arith +
+PNat = Main +
typedef
pnat = "lfp(%X. {1} Un (Suc``X))" (lfp_def)
--- a/src/HOL/Real/PRat.thy Wed May 10 21:04:16 2000 +0200
+++ b/src/HOL/Real/PRat.thy Wed May 10 22:34:30 2000 +0200
@@ -5,7 +5,7 @@
Description : The positive rationals
*)
-PRat = PNat + Equiv +
+PRat = PNat +
constdefs
ratrel :: "((pnat * pnat) * (pnat * pnat)) set"
--- a/src/HOL/Real/ROOT.ML Wed May 10 21:04:16 2000 +0200
+++ b/src/HOL/Real/ROOT.ML Wed May 10 22:34:30 2000 +0200
@@ -13,7 +13,6 @@
time_use_thy "RealDef";
use "simproc.ML";
time_use_thy "Real";
-time_use_thy "Hyperreal/Filter";
time_use_thy "Hyperreal/HyperDef";
(*FIXME: move to RealBin and eliminate all references to 0r, 1r in
--- a/src/HOL/Real/RealAbs.thy Wed May 10 21:04:16 2000 +0200
+++ b/src/HOL/Real/RealAbs.thy Wed May 10 22:34:30 2000 +0200
@@ -5,6 +5,6 @@
Description : Absolute value function for the reals
*)
-RealAbs = RealOrd + RealBin +
+RealAbs = RealBin +
end
--- a/src/HOL/Real/RealBin.thy Wed May 10 21:04:16 2000 +0200
+++ b/src/HOL/Real/RealBin.thy Wed May 10 22:34:30 2000 +0200
@@ -8,7 +8,7 @@
This case is reduced to that for the integers
*)
-RealBin = RealInt + IntArith +
+RealBin = RealInt +
instance
real :: number
--- a/src/HOL/Real/RealInt.ML Wed May 10 21:04:16 2000 +0200
+++ b/src/HOL/Real/RealInt.ML Wed May 10 22:34:30 2000 +0200
@@ -80,14 +80,15 @@
Goal "real_of_int (int (Suc n)) = real_of_int (int n) + 1r";
by (simp_tac (simpset() addsimps [real_of_int_one RS sym,
- real_of_int_add,zadd_int]) 1);
+ real_of_int_add,zadd_int] @ zadd_ac) 1);
qed "real_of_int_Suc";
(* relating two of the embeddings *)
Goal "real_of_int (int n) = real_of_nat n";
by (induct_tac "n" 1);
-by (auto_tac (claset(),simpset() addsimps [real_of_int_zero,
- real_of_nat_zero,real_of_int_Suc,real_of_nat_Suc]));
+by (ALLGOALS (simp_tac (HOL_ss addsimps [real_of_int_zero,
+ real_of_nat_zero,real_of_int_Suc,real_of_nat_Suc])));
+by (Simp_tac 1);
qed "real_of_int_real_of_nat";
Goal "~neg z ==> real_of_nat (nat z) = real_of_int z";
@@ -104,7 +105,7 @@
Goal "(real_of_int x = 0r) = (x = int 0)";
by (auto_tac (claset() addIs [inj_real_of_int RS injD],
- simpset() addsimps [real_of_int_zero]));
+ HOL_ss addsimps [real_of_int_zero]));
qed "real_of_int_zero_cancel";
Addsimps [real_of_int_zero_cancel];
@@ -118,7 +119,7 @@
Goal "x < y ==> (real_of_int x < real_of_int y)";
by (auto_tac (claset(),
- simpset() addsimps [zless_iff_Suc_zadd, real_of_int_add RS sym,
+ HOL_ss addsimps [zless_iff_Suc_zadd, real_of_int_add RS sym,
real_of_int_real_of_nat,
real_of_nat_Suc]));
by (simp_tac (simpset() addsimps [real_of_nat_one RS
--- a/src/HOL/Real/RealInt.thy Wed May 10 21:04:16 2000 +0200
+++ b/src/HOL/Real/RealInt.thy Wed May 10 22:34:30 2000 +0200
@@ -5,7 +5,7 @@
Description: Embedding the integers in the reals
*)
-RealInt = RealOrd + Int +
+RealInt = RealOrd +
constdefs
real_of_int :: int => real
--- a/src/HOL/Real/RealOrd.ML Wed May 10 21:04:16 2000 +0200
+++ b/src/HOL/Real/RealOrd.ML Wed May 10 22:34:30 2000 +0200
@@ -812,7 +812,8 @@
by (dtac lemma_nat_not_dense 1);
by (auto_tac (claset(),
simpset() addsimps [real_of_nat_Suc, real_of_nat_zero] @
- real_add_ac));
+ real_add_ac
+ delsimprocs Nat_Numeral_Simprocs.cancel_numerals));
by (asm_full_simp_tac (simpset() addsimps [real_of_nat_one RS sym,
real_of_nat_add,Suc_diff_n]) 1);
qed "real_of_nat_minus";
--- a/src/HOL/Real/RealPow.thy Wed May 10 21:04:16 2000 +0200
+++ b/src/HOL/Real/RealPow.thy Wed May 10 22:34:30 2000 +0200
@@ -6,11 +6,11 @@
*)
-RealPow = WF_Rel + RealAbs +
+RealPow = RealAbs +
instance real :: {power}
-primrec
+primrec (realpow)
realpow_0 "r ^ 0 = 1r"
realpow_Suc "r ^ (Suc n) = (r::real) * (r ^ n)"