# HG changeset patch
# User Norbert Schirmer <nschirmer@apple.com>
# Date 1635261256 -7200
# Node ID 2f28a0a758abc58514c47605d3a1654c8ca9873b
# Parent  66f10c877542febfd2dbaf8d28d334cbb801554c
fix latex

diff -r 66f10c877542 -r 2f28a0a758ab src/HOL/Statespace/StateSpaceEx.thy
--- a/src/HOL/Statespace/StateSpaceEx.thy	Tue Oct 26 16:01:05 2021 +0200
+++ b/src/HOL/Statespace/StateSpaceEx.thy	Tue Oct 26 17:14:16 2021 +0200
@@ -222,7 +222,7 @@
 
 
 text \<open>Sharing of names in side-by-side statespaces is also possible as long as they are mapped
-to the same type.}\<close>
+to the same type.\<close>
 
 statespace vars1 = n::nat m::nat
 statespace vars2 = n::nat k::nat