# HG changeset patch
# User haftmann
# Date 1664874759 0
# Node ID e19d4c1c48cec5b8426fb62b794e8aeb73da34e2
# Parent  c9ea813f92f217b965b2c303bfee793542385a99
spelling

diff -r c9ea813f92f2 -r e19d4c1c48ce src/HOL/Library/Rounded_Division.thy
--- a/src/HOL/Library/Rounded_Division.thy	Tue Oct 04 09:12:38 2022 +0000
+++ b/src/HOL/Library/Rounded_Division.thy	Tue Oct 04 09:12:39 2022 +0000
@@ -1,7 +1,7 @@
 (*  Author:  Florian Haftmann, TU Muenchen
 *)
 
-subsection \<open>Rounded division: modulus centered towars zero.\<close>
+subsection \<open>Rounded division: modulus centered towards zero.\<close>
 
 theory Rounded_Division
   imports Main