fix latex
authorNorbert Schirmer <nschirmer@apple.com>
Tue, 26 Oct 2021 17:14:16 +0200
changeset 74594 2f28a0a758ab
parent 74593 66f10c877542
child 74595 71bafd70acbb
fix latex
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