--- a/src/HOL/Library/Signed_Division.thy Tue Apr 11 11:59:02 2023 +0000
+++ b/src/HOL/Library/Signed_Division.thy Tue Apr 11 11:59:06 2023 +0000
@@ -47,6 +47,13 @@
end
+text \<open>
+ \noindent The following specification of division is named ``T-division'' in \cite{leijen01}.
+ It is motivated by ISO C99, which in turn adopted the typical behavior of
+ hardware modern in the beginning of the 1990ies; but note ISO C99 describes
+ the instance on machine words, not mathematical integers.
+\<close>
+
instantiation int :: signed_division
begin