renamed axclass_xxxx axclasses
authorobua
Tue Sep 19 18:13:10 2006 +0200 (2006-09-19)
changeset 206095681da8c12ef
parent 20608 86cb35b93f01
child 20610 09ef37366a31
renamed axclass_xxxx axclasses
src/HOL/Ring_and_Field.thy
     1.1 --- a/src/HOL/Ring_and_Field.thy	Tue Sep 19 15:44:04 2006 +0200
     1.2 +++ b/src/HOL/Ring_and_Field.thy	Tue Sep 19 18:13:10 2006 +0200
     1.3 @@ -52,16 +52,16 @@
     1.4  
     1.5  instance comm_semiring_0_cancel \<subseteq> semiring_0_cancel ..
     1.6  
     1.7 -axclass axclass_0_neq_1 \<subseteq> zero, one
     1.8 +axclass zero_neq_one \<subseteq> zero, one
     1.9    zero_neq_one [simp]: "0 \<noteq> 1"
    1.10  
    1.11 -axclass semiring_1 \<subseteq> axclass_0_neq_1, semiring_0, monoid_mult
    1.12 +axclass semiring_1 \<subseteq> zero_neq_one, semiring_0, monoid_mult
    1.13  
    1.14 -axclass comm_semiring_1 \<subseteq> axclass_0_neq_1, comm_semiring_0, comm_monoid_mult (* previously almost_semiring *)
    1.15 +axclass comm_semiring_1 \<subseteq> zero_neq_one, comm_semiring_0, comm_monoid_mult (* previously almost_semiring *)
    1.16  
    1.17  instance comm_semiring_1 \<subseteq> semiring_1 ..
    1.18  
    1.19 -axclass axclass_no_zero_divisors \<subseteq> zero, times
    1.20 +axclass no_zero_divisors \<subseteq> zero, times
    1.21    no_zero_divisors: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0"
    1.22  
    1.23  axclass semiring_1_cancel \<subseteq> semiring_1, cancel_ab_semigroup_add
    1.24 @@ -94,7 +94,7 @@
    1.25  
    1.26  instance comm_ring_1 \<subseteq> comm_semiring_1_cancel ..
    1.27  
    1.28 -axclass idom \<subseteq> comm_ring_1, axclass_no_zero_divisors
    1.29 +axclass idom \<subseteq> comm_ring_1, no_zero_divisors
    1.30  
    1.31  axclass division_ring \<subseteq> ring_1, inverse
    1.32    left_inverse [simp]:  "a \<noteq> 0 ==> inverse a * a = 1"
    1.33 @@ -438,7 +438,7 @@
    1.34    thus "(0::'a) < 1" by (simp add: order_le_less) 
    1.35  qed
    1.36  
    1.37 -instance ordered_ring_strict \<subseteq> axclass_no_zero_divisors 
    1.38 +instance ordered_ring_strict \<subseteq> no_zero_divisors 
    1.39  by (intro_classes, simp)
    1.40  
    1.41  instance ordered_idom \<subseteq> idom ..