# HG changeset patch
# User obua
# Date 1158682390 -7200
# Node ID 5681da8c12ef82a58ca084f9a16cde13c0fd24ea
# Parent  86cb35b93f01901acb2828a7d36a0146ae0946f3
renamed axclass_xxxx axclasses

diff -r 86cb35b93f01 -r 5681da8c12ef src/HOL/Ring_and_Field.thy
--- a/src/HOL/Ring_and_Field.thy	Tue Sep 19 15:44:04 2006 +0200
+++ b/src/HOL/Ring_and_Field.thy	Tue Sep 19 18:13:10 2006 +0200
@@ -52,16 +52,16 @@
 
 instance comm_semiring_0_cancel \<subseteq> semiring_0_cancel ..
 
-axclass axclass_0_neq_1 \<subseteq> zero, one
+axclass zero_neq_one \<subseteq> zero, one
   zero_neq_one [simp]: "0 \<noteq> 1"
 
-axclass semiring_1 \<subseteq> axclass_0_neq_1, semiring_0, monoid_mult
+axclass semiring_1 \<subseteq> zero_neq_one, semiring_0, monoid_mult
 
-axclass comm_semiring_1 \<subseteq> axclass_0_neq_1, comm_semiring_0, comm_monoid_mult (* previously almost_semiring *)
+axclass comm_semiring_1 \<subseteq> zero_neq_one, comm_semiring_0, comm_monoid_mult (* previously almost_semiring *)
 
 instance comm_semiring_1 \<subseteq> semiring_1 ..
 
-axclass axclass_no_zero_divisors \<subseteq> zero, times
+axclass no_zero_divisors \<subseteq> zero, times
   no_zero_divisors: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0"
 
 axclass semiring_1_cancel \<subseteq> semiring_1, cancel_ab_semigroup_add
@@ -94,7 +94,7 @@
 
 instance comm_ring_1 \<subseteq> comm_semiring_1_cancel ..
 
-axclass idom \<subseteq> comm_ring_1, axclass_no_zero_divisors
+axclass idom \<subseteq> comm_ring_1, no_zero_divisors
 
 axclass division_ring \<subseteq> ring_1, inverse
   left_inverse [simp]:  "a \<noteq> 0 ==> inverse a * a = 1"
@@ -438,7 +438,7 @@
   thus "(0::'a) < 1" by (simp add: order_le_less) 
 qed
 
-instance ordered_ring_strict \<subseteq> axclass_no_zero_divisors 
+instance ordered_ring_strict \<subseteq> no_zero_divisors 
 by (intro_classes, simp)
 
 instance ordered_idom \<subseteq> idom ..