doc-src/Locales/Locales/Examples3.thy
changeset 35423 6ef9525a5727
parent 33867 52643d0f856d
child 37206 7f2a6f3143ad
--- a/doc-src/Locales/Locales/Examples3.thy	Mon Mar 01 17:45:19 2010 +0100
+++ b/doc-src/Locales/Locales/Examples3.thy	Mon Mar 01 21:41:35 2010 +0100
@@ -63,7 +63,7 @@
 	statements:
 	@{subgoals [display]}
 	This is Presburger arithmetic, which can be solved by the
-	method @{text arith}. *}
+        method @{text arith}. *}
       by arith+
     txt {* \normalsize In order to show the equations, we put ourselves
       in a situation where the lattice theorems can be used in a