--- a/src/HOL/Imperative_HOL/ex/List_Sublist.thy Thu May 26 16:57:14 2016 +0200
+++ b/src/HOL/Imperative_HOL/ex/List_Sublist.thy Thu May 26 17:51:22 2016 +0200
@@ -2,7 +2,7 @@
Author: Lukas Bulwahn, TU Muenchen
*)
-section {* Slices of lists *}
+section \<open>Slices of lists\<close>
theory List_Sublist
imports "~~/src/HOL/Library/Multiset"
@@ -188,7 +188,7 @@
apply auto
done
-section {* Another sublist function *}
+section \<open>Another sublist function\<close>
function sublist' :: "nat \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
where
@@ -199,7 +199,7 @@
by pat_completeness auto
termination by lexicographic_order
-subsection {* Proving equivalence to the other sublist command *}
+subsection \<open>Proving equivalence to the other sublist command\<close>
lemma sublist'_sublist: "sublist' n m xs = sublist xs {j. n \<le> j \<and> j < m}"
apply (induct xs arbitrary: n m)
@@ -227,7 +227,7 @@
done
-subsection {* Showing equivalence to use of drop and take for definition *}
+subsection \<open>Showing equivalence to use of drop and take for definition\<close>
lemma "sublist' n m xs = take (m - n) (drop n xs)"
apply (induct xs arbitrary: n m)
@@ -239,7 +239,7 @@
apply simp
done
-subsection {* General lemma about sublist *}
+subsection \<open>General lemma about sublist\<close>
lemma sublist'_Nil[simp]: "sublist' i j [] = []"
by simp