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)
```