--- a/src/HOL/ex/Seq.thy Tue Oct 07 21:01:31 2014 +0200 +++ b/src/HOL/ex/Seq.thy Tue Oct 07 21:11:18 2014 +0200 @@ -2,7 +2,7 @@ Author: Makarius *) -header {* Finite sequences *} +header \<open>Finite sequences\<close> theory Seq imports Main