# HG changeset patch
# User haftmann
# Date 1699724643 0
# Node ID 74147aa81dbb0e560e51abb71934bacb65614914
# Parent  db9dba720ac7d5de9da13a1c997563d71d04c688
more specific name for type class

diff -r db9dba720ac7 -r 74147aa81dbb NEWS
--- a/NEWS	Sat Nov 11 22:17:14 2023 +0100
+++ b/NEWS	Sat Nov 11 17:44:03 2023 +0000
@@ -21,7 +21,9 @@
 * Type class linordered_euclidean_semiring replaces the (rather technical)
   type class unique_euclidean_semiring_with_nat;  type class
   unique_euclidean_ring_with_nat, which barely admits instances other than
-  isomorphic to int, is discontinued.  Minor INCOMPATIBILITY.
+  isomorphic to int, is discontinued;  type class
+  unique_euclidean_semiring_with_bit_operations is renamed
+  to linordered_euclidean_semiring_bit_operations.  Minor INCOMPATIBILITY.
 
 
 *** ML ***
diff -r db9dba720ac7 -r 74147aa81dbb src/HOL/Bit_Operations.thy
--- a/src/HOL/Bit_Operations.thy	Sat Nov 11 22:17:14 2023 +0100
+++ b/src/HOL/Bit_Operations.thy	Sat Nov 11 17:44:03 2023 +0000
@@ -2625,7 +2625,7 @@
 
 subsection \<open>Common algebraic structure\<close>
 
-class unique_euclidean_semiring_with_bit_operations =
+class linordered_euclidean_semiring_bit_operations =
   linordered_euclidean_semiring + semiring_bit_operations
 begin
 
@@ -2737,9 +2737,9 @@
 
 end
 
-instance nat :: unique_euclidean_semiring_with_bit_operations ..
-
-instance int :: unique_euclidean_semiring_with_bit_operations ..
+instance nat :: linordered_euclidean_semiring_bit_operations ..
+
+instance int :: linordered_euclidean_semiring_bit_operations ..
 
 lemma drop_bit_Suc_minus_bit0 [simp]:
   \<open>drop_bit (Suc n) (- numeral (Num.Bit0 k)) = drop_bit n (- numeral k :: int)\<close>
@@ -2802,7 +2802,7 @@
 
 end
 
-context unique_euclidean_semiring_with_bit_operations
+context linordered_euclidean_semiring_bit_operations
 begin
 
 lemma bit_numeral_iff:
@@ -3655,7 +3655,7 @@
 
 end
 
-context unique_euclidean_semiring_with_bit_operations
+context linordered_euclidean_semiring_bit_operations
 begin
 
 lemma bit_horner_sum_bit_iff [bit_simps]:
diff -r db9dba720ac7 -r 74147aa81dbb src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Sat Nov 11 22:17:14 2023 +0100
+++ b/src/HOL/Code_Numeral.thy	Sat Nov 11 17:44:03 2023 +0000
@@ -357,7 +357,7 @@
 
 end
 
-instance integer :: unique_euclidean_semiring_with_bit_operations ..
+instance integer :: linordered_euclidean_semiring_bit_operations ..
 
 context
   includes bit_operations_syntax
@@ -1115,7 +1115,7 @@
 
 end
 
-instance natural :: unique_euclidean_semiring_with_bit_operations ..
+instance natural :: linordered_euclidean_semiring_bit_operations ..
 
 context
   includes bit_operations_syntax
diff -r db9dba720ac7 -r 74147aa81dbb src/HOL/Library/Word.thy
--- a/src/HOL/Library/Word.thy	Sat Nov 11 22:17:14 2023 +0100
+++ b/src/HOL/Library/Word.thy	Sat Nov 11 17:44:03 2023 +0000
@@ -1143,7 +1143,7 @@
 
 end
 
-context unique_euclidean_semiring_with_bit_operations
+context linordered_euclidean_semiring_bit_operations
 begin
 
 lemma unsigned_drop_bit_eq:
diff -r db9dba720ac7 -r 74147aa81dbb src/HOL/String.thy
--- a/src/HOL/String.thy	Sat Nov 11 22:17:14 2023 +0100
+++ b/src/HOL/String.thy	Sat Nov 11 17:44:03 2023 +0000
@@ -51,7 +51,7 @@
   by (cases c) (simp only: of_char_Char nat_horner_sum)
 
 
-context unique_euclidean_semiring_with_bit_operations
+context linordered_euclidean_semiring_bit_operations
 begin
 
 definition char_of :: \<open>'a \<Rightarrow> char\<close>
@@ -439,7 +439,7 @@
 
 end
 
-context unique_euclidean_semiring_with_bit_operations
+context linordered_euclidean_semiring_bit_operations
 begin
 
 context