--- a/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy Wed Dec 30 21:57:52 2015 +0100
@@ -93,7 +93,7 @@
by (simp add: Map_def Consq_def flift2_def)
-subsubsection {* Filter *}
+subsubsection \<open>Filter\<close>
lemma Filter_UU: "Filter P$UU =UU"
by (simp add: Filter_def)
@@ -106,7 +106,7 @@
by (simp add: Filter_def Consq_def flift2_def If_and_if)
-subsubsection {* Forall *}
+subsubsection \<open>Forall\<close>
lemma Forall_UU: "Forall P UU"
by (simp add: Forall_def sforall_def)
@@ -118,13 +118,13 @@
by (simp add: Forall_def sforall_def Consq_def flift2_def)
-subsubsection {* Conc *}
+subsubsection \<open>Conc\<close>
lemma Conc_cons: "(x\<leadsto>xs) @@ y = x\<leadsto>(xs @@y)"
by (simp add: Consq_def)
-subsubsection {* Takewhile *}
+subsubsection \<open>Takewhile\<close>
lemma Takewhile_UU: "Takewhile P$UU =UU"
by (simp add: Takewhile_def)
@@ -137,7 +137,7 @@
by (simp add: Takewhile_def Consq_def flift2_def If_and_if)
-subsubsection {* DropWhile *}
+subsubsection \<open>DropWhile\<close>
lemma Dropwhile_UU: "Dropwhile P$UU =UU"
by (simp add: Dropwhile_def)
@@ -150,7 +150,7 @@
by (simp add: Dropwhile_def Consq_def flift2_def If_and_if)
-subsubsection {* Last *}
+subsubsection \<open>Last\<close>
lemma Last_UU: "Last$UU =UU"
by (simp add: Last_def)
@@ -165,7 +165,7 @@
done
-subsubsection {* Flat *}
+subsubsection \<open>Flat\<close>
lemma Flat_UU: "Flat$UU =UU"
by (simp add: Flat_def)
@@ -177,7 +177,7 @@
by (simp add: Flat_def Consq_def)
-subsubsection {* Zip *}
+subsubsection \<open>Zip\<close>
lemma Zip_unfold:
"Zip = (LAM t1 t2. case t1 of
@@ -1075,7 +1075,7 @@
done
-ML {*
+ML \<open>
fun Seq_case_tac ctxt s i =
Rule_Insts.res_inst_tac ctxt [((("x", 0), Position.none), s)] [] @{thm Seq_cases} i
@@ -1109,6 +1109,6 @@
THEN (REPEAT_DETERM (CHANGED (simp_tac ctxt (i+1))))
THEN simp_tac (ctxt addsimps rws) i;
-*}
+\<close>
end