src/HOL/HOLCF/Cprod.thy

 (*  Title:      HOL/HOLCF/Cprod.thy
     Author:     Franz Regensburger
 *)
 
-section {* The cpo of cartesian products *}
+section \<open>The cpo of cartesian products\<close>
 
 theory Cprod
 imports Cfun
 begin
 
 default_sort cpo
 
-subsection {* Continuous case function for unit type *}
+subsection \<open>Continuous case function for unit type\<close>
 
 definition
   unit_when :: "'a \<rightarrow> unit \<rightarrow> 'a" where
   "unit_when = (\<Lambda> a _. a)"
 

   "\<Lambda>(). t" == "CONST unit_when\<cdot>t"
 
 lemma unit_when [simp]: "unit_when\<cdot>a\<cdot>u = a"
 by (simp add: unit_when_def)
 
-subsection {* Continuous version of split function *}
+subsection \<open>Continuous version of split function\<close>
 
 definition
   csplit :: "('a \<rightarrow> 'b \<rightarrow> 'c) \<rightarrow> ('a * 'b) \<rightarrow> 'c" where
   "csplit = (\<Lambda> f p. f\<cdot>(fst p)\<cdot>(snd p))"
 

 
 abbreviation
   csnd :: "'a \<times> 'b \<rightarrow> 'b" where
   "csnd \<equiv> Abs_cfun snd"
 
-subsection {* Convert all lemmas to the continuous versions *}
+subsection \<open>Convert all lemmas to the continuous versions\<close>
 
 lemma csplit1 [simp]: "csplit\<cdot>f\<cdot>\<bottom> = f\<cdot>\<bottom>\<cdot>\<bottom>"
 by (simp add: csplit_def)
 
 lemma csplit_Pair [simp]: "csplit\<cdot>f\<cdot>(x, y) = f\<cdot>x\<cdot>y"