--- a/src/HOL/Library/Signed_Division.thy Sat Oct 01 07:56:53 2022 +0000
+++ b/src/HOL/Library/Signed_Division.thy Sat Oct 01 13:08:34 2022 +0000
@@ -7,9 +7,13 @@
imports Main
begin
-class signed_division = comm_semiring_1_cancel +
+class signed_divide =
fixes signed_divide :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close> (infixl \<open>sdiv\<close> 70)
- and signed_modulo :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close> (infixl \<open>smod\<close> 70)
+
+class signed_modulo =
+ fixes signed_modulo :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close> (infixl \<open>smod\<close> 70)
+
+class signed_division = comm_semiring_1_cancel + signed_divide + signed_modulo +
assumes sdiv_mult_smod_eq: \<open>a sdiv b * b + a smod b = a\<close>
begin