--- 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 ***
--- 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]:
--- 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
--- 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:
--- 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