src/HOL/HOLCF/IOA/meta_theory/Sequence.thy

 
 lemma Map_cons: "Map f$(x\<leadsto>xs)=(f x) \<leadsto> Map f$xs"
 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)
 
 lemma Filter_nil: "Filter P$nil =nil"

 lemma Filter_cons:
   "Filter P$(x\<leadsto>xs)= (if P x then x\<leadsto>(Filter P$xs) else Filter P$xs)"
 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)
 
 lemma Forall_nil: "Forall P nil"

 
 lemma Forall_cons: "Forall P (x\<leadsto>xs)= (P x & Forall P xs)"
 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)
 
 lemma Takewhile_nil: "Takewhile P$nil =nil"

 lemma Takewhile_cons:
   "Takewhile P$(x\<leadsto>xs)= (if P x then x\<leadsto>(Takewhile P$xs) else nil)"
 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)
 
 lemma Dropwhile_nil: "Dropwhile P$nil =nil"

 lemma Dropwhile_cons:
   "Dropwhile P$(x\<leadsto>xs)= (if P x then Dropwhile P$xs else x\<leadsto>xs)"
 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)
 
 lemma Last_nil: "Last$nil =UU"

 apply (cases xs)
 apply simp_all
 done
 
 
-subsubsection {* Flat *}
+subsubsection \<open>Flat\<close>
 
 lemma Flat_UU: "Flat$UU =UU"
 by (simp add: Flat_def)
 
 lemma Flat_nil: "Flat$nil =nil"

 
 lemma Flat_cons: "Flat$(x##xs)= x @@ (Flat$xs)"
 by (simp add: Flat_def Consq_def)
 
 
-subsubsection {* Zip *}
+subsubsection \<open>Zip\<close>
 
 lemma Zip_unfold:
 "Zip = (LAM t1 t2. case t1 of
                 nil   => nil
               | x##xs => (case t2 of

     take_lemma_in_eq_out [THEN mp])
 apply auto
 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
   THEN hyp_subst_tac ctxt i THEN hyp_subst_tac ctxt (i+1) THEN hyp_subst_tac ctxt (i+2);
 

   Rule_Insts.res_inst_tac ctxt [((("x", 0), Position.none), s)] [] @{thm Seq_induct} i
   THEN pair_tac ctxt "a" (i+3)
   THEN (REPEAT_DETERM (CHANGED (simp_tac ctxt (i+1))))
   THEN simp_tac (ctxt addsimps rws) i;
 
-*}
+\<close>
 
 end