--- a/src/HOL/Hyperreal/NSA.thy Tue Sep 19 23:18:41 2006 +0200
+++ b/src/HOL/Hyperreal/NSA.thy Wed Sep 20 00:24:24 2006 +0200
@@ -954,7 +954,7 @@
(*again: 1 is a special case, but not 0 this time*)
lemma one_not_Infinitesimal [simp]:
- "(1::'a::{real_normed_vector,axclass_0_neq_1} star) \<notin> Infinitesimal"
+ "(1::'a::{real_normed_vector,zero_neq_one} star) \<notin> Infinitesimal"
apply (simp only: star_one_def star_of_Infinitesimal_iff_0)
apply simp
done
@@ -1032,8 +1032,8 @@
(number_of w = (1::'b))"
"((1::'b::{number,one,real_normed_vector} star) @= number_of w) =
(number_of w = (1::'b))"
- "~ (0 @= (1::'c::{axclass_0_neq_1,real_normed_vector} star))"
- "~ (1 @= (0::'c::{axclass_0_neq_1,real_normed_vector} star))"
+ "~ (0 @= (1::'c::{zero_neq_one,real_normed_vector} star))"
+ "~ (1 @= (0::'c::{zero_neq_one,real_normed_vector} star))"
apply (unfold star_number_def star_zero_def star_one_def)
apply (unfold star_of_approx_iff)
by (auto intro: sym)
--- a/src/HOL/Hyperreal/StarClasses.thy Tue Sep 19 23:18:41 2006 +0200
+++ b/src/HOL/Hyperreal/StarClasses.thy Wed Sep 20 00:24:24 2006 +0200
@@ -283,13 +283,13 @@
instance star :: (comm_semiring_0) comm_semiring_0 ..
instance star :: (comm_semiring_0_cancel) comm_semiring_0_cancel ..
-instance star :: (axclass_0_neq_1) axclass_0_neq_1
+instance star :: (zero_neq_one) zero_neq_one
by (intro_classes, transfer, rule zero_neq_one)
instance star :: (semiring_1) semiring_1 ..
instance star :: (comm_semiring_1) comm_semiring_1 ..
-instance star :: (axclass_no_zero_divisors) axclass_no_zero_divisors
+instance star :: (no_zero_divisors) no_zero_divisors
by (intro_classes, transfer, rule no_zero_divisors)
instance star :: (semiring_1_cancel) semiring_1_cancel ..
@@ -340,7 +340,7 @@
instance star :: (pordered_ring) pordered_ring ..
instance star :: (lordered_ring) lordered_ring ..
-instance star :: (axclass_abs_if) axclass_abs_if
+instance star :: (abs_if) abs_if
by (intro_classes, transfer, rule abs_if)
instance star :: (ordered_ring_strict) ordered_ring_strict ..
--- a/src/HOL/Matrix/Matrix.thy Tue Sep 19 23:18:41 2006 +0200
+++ b/src/HOL/Matrix/Matrix.thy Wed Sep 20 00:24:24 2006 +0200
@@ -132,14 +132,14 @@
apply (rule exI[of _ n], simp add: split_if)+
by (simp add: split_if)
-lemma nrows_one_matrix[simp]: "nrows ((one_matrix n) :: ('a::axclass_0_neq_1)matrix) = n" (is "?r = _")
+lemma nrows_one_matrix[simp]: "nrows ((one_matrix n) :: ('a::zero_neq_one)matrix) = n" (is "?r = _")
proof -
have "?r <= n" by (simp add: nrows_le)
moreover have "n <= ?r" by (simp add:le_nrows, arith)
ultimately show "?r = n" by simp
qed
-lemma ncols_one_matrix[simp]: "ncols ((one_matrix n) :: ('a::axclass_0_neq_1)matrix) = n" (is "?r = _")
+lemma ncols_one_matrix[simp]: "ncols ((one_matrix n) :: ('a::zero_neq_one)matrix) = n" (is "?r = _")
proof -
have "?r <= n" by (simp add: ncols_le)
moreover have "n <= ?r" by (simp add: le_ncols, arith)
--- a/src/HOL/Ring_and_Field.thy Tue Sep 19 23:18:41 2006 +0200
+++ b/src/HOL/Ring_and_Field.thy Wed Sep 20 00:24:24 2006 +0200
@@ -241,10 +241,10 @@
instance lordered_ring \<subseteq> lordered_ab_group_join ..
-axclass axclass_abs_if \<subseteq> minus, ord, zero
+axclass abs_if \<subseteq> minus, ord, zero
abs_if: "abs a = (if (a < 0) then (-a) else a)"
-axclass ordered_ring_strict \<subseteq> ring, ordered_semiring_strict, axclass_abs_if
+axclass ordered_ring_strict \<subseteq> ring, ordered_semiring_strict, abs_if
instance ordered_ring_strict \<subseteq> lordered_ab_group ..
@@ -256,7 +256,7 @@
axclass ordered_semidom \<subseteq> comm_semiring_1_cancel, ordered_comm_semiring_strict (* previously ordered_semiring *)
zero_less_one [simp]: "0 < 1"
-axclass ordered_idom \<subseteq> comm_ring_1, ordered_comm_semiring_strict, axclass_abs_if (* previously ordered_ring *)
+axclass ordered_idom \<subseteq> comm_ring_1, ordered_comm_semiring_strict, abs_if (* previously ordered_ring *)
instance ordered_idom \<subseteq> ordered_ring_strict ..