# HG changeset patch
# User wenzelm
# Date 1158704664 -7200
# Node ID e98f59806244598114bcdca2791c1dd5eda619f9
# Parent  40abbc7c86df1e370dbc7570040fdd300f85d05c
renamed axclass_xxxx axclasses;

diff -r 40abbc7c86df -r e98f59806244 src/HOL/Hyperreal/NSA.thy
--- 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)
diff -r 40abbc7c86df -r e98f59806244 src/HOL/Hyperreal/StarClasses.thy
--- 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 ..
diff -r 40abbc7c86df -r e98f59806244 src/HOL/Matrix/Matrix.thy
--- 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)
diff -r 40abbc7c86df -r e98f59806244 src/HOL/Ring_and_Field.thy
--- 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 ..