changeset 77811 | ae9e6218443d |
parent 76232 | a7ccb744047b |
child 77812 | fb3d81bd9803 |
--- a/src/HOL/Library/Signed_Division.thy Mon Apr 10 23:21:47 2023 +0200 +++ b/src/HOL/Library/Signed_Division.thy Tue Apr 11 11:59:02 2023 +0000 @@ -1,7 +1,7 @@ (* Author: Stefan Berghofer et al. *) -subsection \<open>Signed division: negative results rounded towards zero rather than minus infinity.\<close> +section \<open>Signed division: negative results rounded towards zero rather than minus infinity.\<close> theory Signed_Division imports Main