src/HOL/HOLCF/Tr.thy
changeset 62175 8ffc4d0e652d
parent 58956 a816aa3ff391
child 67312 0d25e02759b7
     1.1 --- a/src/HOL/HOLCF/Tr.thy	Wed Jan 13 23:02:28 2016 +0100
     1.2 +++ b/src/HOL/HOLCF/Tr.thy	Wed Jan 13 23:07:06 2016 +0100
     1.3 @@ -2,13 +2,13 @@
     1.4      Author:     Franz Regensburger
     1.5  *)
     1.6  
     1.7 -section {* The type of lifted booleans *}
     1.8 +section \<open>The type of lifted booleans\<close>
     1.9  
    1.10  theory Tr
    1.11  imports Lift
    1.12  begin
    1.13  
    1.14 -subsection {* Type definition and constructors *}
    1.15 +subsection \<open>Type definition and constructors\<close>
    1.16  
    1.17  type_synonym
    1.18    tr = "bool lift"
    1.19 @@ -24,7 +24,7 @@
    1.20    FF :: "tr" where
    1.21    "FF = Def False"
    1.22  
    1.23 -text {* Exhaustion and Elimination for type @{typ tr} *}
    1.24 +text \<open>Exhaustion and Elimination for type @{typ tr}\<close>
    1.25  
    1.26  lemma Exh_tr: "t = \<bottom> \<or> t = TT \<or> t = FF"
    1.27  unfolding FF_def TT_def by (induct t) auto
    1.28 @@ -37,7 +37,7 @@
    1.29    "\<lbrakk>P \<bottom>; P TT; P FF\<rbrakk> \<Longrightarrow> P x"
    1.30  by (cases x) simp_all
    1.31  
    1.32 -text {* distinctness for type @{typ tr} *}
    1.33 +text \<open>distinctness for type @{typ tr}\<close>
    1.34  
    1.35  lemma dist_below_tr [simp]:
    1.36    "TT \<notsqsubseteq> \<bottom>" "FF \<notsqsubseteq> \<bottom>" "TT \<notsqsubseteq> FF" "FF \<notsqsubseteq> TT"
    1.37 @@ -60,7 +60,7 @@
    1.38  by (induct x) simp_all
    1.39  
    1.40  
    1.41 -subsection {* Case analysis *}
    1.42 +subsection \<open>Case analysis\<close>
    1.43  
    1.44  default_sort pcpo
    1.45  
    1.46 @@ -83,7 +83,7 @@
    1.47  by (simp_all add: tr_case_def TT_def FF_def)
    1.48  
    1.49  
    1.50 -subsection {* Boolean connectives *}
    1.51 +subsection \<open>Boolean connectives\<close>
    1.52  
    1.53  definition
    1.54    trand :: "tr \<rightarrow> tr \<rightarrow> tr" where
    1.55 @@ -107,11 +107,11 @@
    1.56    If2 :: "[tr, 'c, 'c] \<Rightarrow> 'c" where
    1.57    "If2 Q x y = (If Q then x else y)"
    1.58  
    1.59 -text {* tactic for tr-thms with case split *}
    1.60 +text \<open>tactic for tr-thms with case split\<close>
    1.61  
    1.62  lemmas tr_defs = andalso_def orelse_def neg_def tr_case_def TT_def FF_def
    1.63  
    1.64 -text {* lemmas about andalso, orelse, neg and if *}
    1.65 +text \<open>lemmas about andalso, orelse, neg and if\<close>
    1.66  
    1.67  lemma andalso_thms [simp]:
    1.68    "(TT andalso y) = y"
    1.69 @@ -141,7 +141,7 @@
    1.70    "neg\<cdot>\<bottom> = \<bottom>"
    1.71  by (simp_all add: neg_def TT_def FF_def)
    1.72  
    1.73 -text {* split-tac for If via If2 because the constant has to be a constant *}
    1.74 +text \<open>split-tac for If via If2 because the constant has to be a constant\<close>
    1.75  
    1.76  lemma split_If2:
    1.77    "P (If2 Q x y) = ((Q = \<bottom> \<longrightarrow> P \<bottom>) \<and> (Q = TT \<longrightarrow> P x) \<and> (Q = FF \<longrightarrow> P y))"
    1.78 @@ -151,11 +151,11 @@
    1.79  done
    1.80  
    1.81  (* FIXME unused!? *)
    1.82 -ML {*
    1.83 +ML \<open>
    1.84  fun split_If_tac ctxt =
    1.85    simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm If2_def} RS sym])
    1.86      THEN' (split_tac ctxt [@{thm split_If2}])
    1.87 -*}
    1.88 +\<close>
    1.89  
    1.90  subsection "Rewriting of HOLCF operations to HOL functions"
    1.91  
    1.92 @@ -189,7 +189,7 @@
    1.93  apply (auto simp add: TT_def[symmetric] FF_def[symmetric])
    1.94  done
    1.95  
    1.96 -subsection {* Compactness *}
    1.97 +subsection \<open>Compactness\<close>
    1.98  
    1.99  lemma compact_TT: "compact TT"
   1.100  by (rule compact_chfin)