remove LaTeX hyperref warnings by avoiding antiquotations within section headings
authorhuffman
Mon Mar 22 12:52:51 2010 -0700 (2010-03-22)
changeset 35900aa5dfb03eb1e
parent 35897 8758895ea413
child 35901 12f09bf2c77f
remove LaTeX hyperref warnings by avoiding antiquotations within section headings
src/HOLCF/Cont.thy
src/HOLCF/Cprod.thy
src/HOLCF/Discrete.thy
src/HOLCF/Pcpodef.thy
src/HOLCF/Product_Cpo.thy
src/HOLCF/Representable.thy
src/HOLCF/Sprod.thy
src/HOLCF/Ssum.thy
src/HOLCF/Sum_Cpo.thy
src/HOLCF/Universal.thy
src/HOLCF/Up.thy
     1.1 --- a/src/HOLCF/Cont.thy	Mon Mar 22 19:29:11 2010 +0100
     1.2 +++ b/src/HOLCF/Cont.thy	Mon Mar 22 12:52:51 2010 -0700
     1.3 @@ -55,7 +55,7 @@
     1.4  by (simp add: monofun_def)
     1.5  
     1.6  
     1.7 -subsection {* @{prop "monofun f \<and> contlub f \<equiv> cont f"} *}
     1.8 +subsection {* Equivalence of alternate definition *}
     1.9  
    1.10  text {* monotone functions map chains to chains *}
    1.11  
     2.1 --- a/src/HOLCF/Cprod.thy	Mon Mar 22 19:29:11 2010 +0100
     2.2 +++ b/src/HOLCF/Cprod.thy	Mon Mar 22 12:52:51 2010 -0700
     2.3 @@ -10,7 +10,7 @@
     2.4  
     2.5  defaultsort cpo
     2.6  
     2.7 -subsection {* Type @{typ unit} is a pcpo *}
     2.8 +subsection {* Continuous case function for unit type *}
     2.9  
    2.10  definition
    2.11    unit_when :: "'a \<rightarrow> unit \<rightarrow> 'a" where
     3.1 --- a/src/HOLCF/Discrete.thy	Mon Mar 22 19:29:11 2010 +0100
     3.2 +++ b/src/HOLCF/Discrete.thy	Mon Mar 22 12:52:51 2010 -0700
     3.3 @@ -10,7 +10,7 @@
     3.4  
     3.5  datatype 'a discr = Discr "'a :: type"
     3.6  
     3.7 -subsection {* Type @{typ "'a discr"} is a discrete cpo *}
     3.8 +subsection {* Discrete ordering *}
     3.9  
    3.10  instantiation discr :: (type) below
    3.11  begin
    3.12 @@ -22,14 +22,14 @@
    3.13  instance ..
    3.14  end
    3.15  
    3.16 +subsection {* Discrete cpo class instance *}
    3.17 +
    3.18  instance discr :: (type) discrete_cpo
    3.19  by intro_classes (simp add: below_discr_def)
    3.20  
    3.21  lemma discr_below_eq [iff]: "((x::('a::type)discr) << y) = (x = y)"
    3.22  by simp (* FIXME: same discrete_cpo - remove? is [iff] important? *)
    3.23  
    3.24 -subsection {* Type @{typ "'a discr"} is a cpo *}
    3.25 -
    3.26  lemma discr_chain0: 
    3.27   "!!S::nat=>('a::type)discr. chain S ==> S i = S 0"
    3.28  apply (unfold chain_def)
    3.29 @@ -60,7 +60,7 @@
    3.30  apply (clarify, erule discr_chain0 [symmetric])
    3.31  done
    3.32  
    3.33 -subsection {* @{term undiscr} *}
    3.34 +subsection {* \emph{undiscr} *}
    3.35  
    3.36  definition
    3.37    undiscr :: "('a::type)discr => 'a" where
     4.1 --- a/src/HOLCF/Pcpodef.thy	Mon Mar 22 19:29:11 2010 +0100
     4.2 +++ b/src/HOLCF/Pcpodef.thy	Mon Mar 22 12:52:51 2010 -0700
     4.3 @@ -129,7 +129,7 @@
     4.4    thus "\<exists>x. range S <<| x" ..
     4.5  qed
     4.6  
     4.7 -subsubsection {* Continuity of @{term Rep} and @{term Abs} *}
     4.8 +subsubsection {* Continuity of \emph{Rep} and \emph{Abs} *}
     4.9  
    4.10  text {* For any sub-cpo, the @{term Rep} function is continuous. *}
    4.11  
    4.12 @@ -229,7 +229,7 @@
    4.13    shows "OFCLASS('b, pcpo_class)"
    4.14  by (rule typedef_pcpo_generic [OF type below UU_in_A], rule minimal)
    4.15  
    4.16 -subsubsection {* Strictness of @{term Rep} and @{term Abs} *}
    4.17 +subsubsection {* Strictness of \emph{Rep} and \emph{Abs} *}
    4.18  
    4.19  text {*
    4.20    For a sub-pcpo where @{term \<bottom>} is a member of the defining
     5.1 --- a/src/HOLCF/Product_Cpo.thy	Mon Mar 22 19:29:11 2010 +0100
     5.2 +++ b/src/HOLCF/Product_Cpo.thy	Mon Mar 22 12:52:51 2010 -0700
     5.3 @@ -10,7 +10,7 @@
     5.4  
     5.5  defaultsort cpo
     5.6  
     5.7 -subsection {* Type @{typ unit} is a pcpo *}
     5.8 +subsection {* Unit type is a pcpo *}
     5.9  
    5.10  instantiation unit :: below
    5.11  begin
    5.12 @@ -58,7 +58,7 @@
    5.13      by (fast intro: below_trans)
    5.14  qed
    5.15  
    5.16 -subsection {* Monotonicity of @{text "(_,_)"}, @{term fst}, @{term snd} *}
    5.17 +subsection {* Monotonicity of \emph{Pair}, \emph{fst}, \emph{snd} *}
    5.18  
    5.19  lemma prod_belowI: "\<lbrakk>fst p \<sqsubseteq> fst q; snd p \<sqsubseteq> snd q\<rbrakk> \<Longrightarrow> p \<sqsubseteq> q"
    5.20  unfolding below_prod_def by simp
    5.21 @@ -187,7 +187,7 @@
    5.22  lemma split_strict [simp]: "split f \<bottom> = f \<bottom> \<bottom>"
    5.23  unfolding split_def by simp
    5.24  
    5.25 -subsection {* Continuity of @{text "(_,_)"}, @{term fst}, @{term snd} *}
    5.26 +subsection {* Continuity of \emph{Pair}, \emph{fst}, \emph{snd} *}
    5.27  
    5.28  lemma cont_pair1: "cont (\<lambda>x. (x, y))"
    5.29  apply (rule contI)
     6.1 --- a/src/HOLCF/Representable.thy	Mon Mar 22 19:29:11 2010 +0100
     6.2 +++ b/src/HOLCF/Representable.thy	Mon Mar 22 12:52:51 2010 -0700
     6.3 @@ -35,7 +35,7 @@
     6.4  lemmas prj_strict = rep.p_strict
     6.5  
     6.6  
     6.7 -subsection {* Making @{term rep} the default class *}
     6.8 +subsection {* Making \emph{rep} the default class *}
     6.9  
    6.10  text {*
    6.11    From now on, free type variables are assumed to be in class
    6.12 @@ -342,7 +342,7 @@
    6.13  use "Tools/repdef.ML"
    6.14  
    6.15  
    6.16 -subsection {* Instances of class @{text rep} *}
    6.17 +subsection {* Instances of class \emph{rep} *}
    6.18  
    6.19  subsubsection {* Universal Domain *}
    6.20  
     7.1 --- a/src/HOLCF/Sprod.thy	Mon Mar 22 19:29:11 2010 +0100
     7.2 +++ b/src/HOLCF/Sprod.thy	Mon Mar 22 12:52:51 2010 -0700
     7.3 @@ -88,7 +88,7 @@
     7.4    "\<lbrakk>P \<bottom>; \<And>x y. \<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> P (:x, y:)\<rbrakk> \<Longrightarrow> P x"
     7.5  by (cases x, simp_all)
     7.6  
     7.7 -subsection {* Properties of @{term spair} *}
     7.8 +subsection {* Properties of \emph{spair} *}
     7.9  
    7.10  lemma spair_strict1 [simp]: "(:\<bottom>, y:) = \<bottom>"
    7.11  by (simp add: Rep_Sprod_simps strictify_conv_if)
    7.12 @@ -134,7 +134,7 @@
    7.13  lemma sprodE2: "(\<And>x y. p = (:x, y:) \<Longrightarrow> Q) \<Longrightarrow> Q"
    7.14  by (cases p, simp only: inst_sprod_pcpo2, simp)
    7.15  
    7.16 -subsection {* Properties of @{term sfst} and @{term ssnd} *}
    7.17 +subsection {* Properties of \emph{sfst} and \emph{ssnd} *}
    7.18  
    7.19  lemma sfst_strict [simp]: "sfst\<cdot>\<bottom> = \<bottom>"
    7.20  by (simp add: sfst_def cont_Rep_Sprod Rep_Sprod_strict)
    7.21 @@ -208,7 +208,7 @@
    7.22  apply simp
    7.23  done
    7.24  
    7.25 -subsection {* Properties of @{term ssplit} *}
    7.26 +subsection {* Properties of \emph{ssplit} *}
    7.27  
    7.28  lemma ssplit1 [simp]: "ssplit\<cdot>f\<cdot>\<bottom> = \<bottom>"
    7.29  by (simp add: ssplit_def)
     8.1 --- a/src/HOLCF/Ssum.thy	Mon Mar 22 19:29:11 2010 +0100
     8.2 +++ b/src/HOLCF/Ssum.thy	Mon Mar 22 12:52:51 2010 -0700
     8.3 @@ -58,7 +58,7 @@
     8.4  lemma Rep_Ssum_sinr: "Rep_Ssum (sinr\<cdot>b) = (strictify\<cdot>(\<Lambda> _. FF)\<cdot>b, \<bottom>, b)"
     8.5  by (simp add: sinr_Abs_Ssum Abs_Ssum_inverse sinr_Ssum)
     8.6  
     8.7 -subsection {* Properties of @{term sinl} and @{term sinr} *}
     8.8 +subsection {* Properties of \emph{sinl} and \emph{sinr} *}
     8.9  
    8.10  text {* Ordering *}
    8.11  
     9.1 --- a/src/HOLCF/Sum_Cpo.thy	Mon Mar 22 19:29:11 2010 +0100
     9.2 +++ b/src/HOLCF/Sum_Cpo.thy	Mon Mar 22 12:52:51 2010 -0700
     9.3 @@ -8,7 +8,7 @@
     9.4  imports Bifinite
     9.5  begin
     9.6  
     9.7 -subsection {* Ordering on type @{typ "'a + 'b"} *}
     9.8 +subsection {* Ordering on sum type *}
     9.9  
    9.10  instantiation "+" :: (below, below) below
    9.11  begin
    9.12 @@ -128,7 +128,7 @@
    9.13   apply (erule cpo_lubI)
    9.14  done
    9.15  
    9.16 -subsection {* Continuity of @{term Inl}, @{term Inr}, @{term sum_case} *}
    9.17 +subsection {* Continuity of \emph{Inl}, \emph{Inr}, and case function *}
    9.18  
    9.19  lemma cont_Inl: "cont Inl"
    9.20  by (intro contI is_lub_Inl cpo_lubI)
    10.1 --- a/src/HOLCF/Universal.thy	Mon Mar 22 19:29:11 2010 +0100
    10.2 +++ b/src/HOLCF/Universal.thy	Mon Mar 22 12:52:51 2010 -0700
    10.3 @@ -187,7 +187,7 @@
    10.4  apply simp
    10.5  done
    10.6  
    10.7 -subsubsection {* Take function for @{typ ubasis} *}
    10.8 +subsubsection {* Take function for \emph{ubasis} *}
    10.9  
   10.10  definition
   10.11    ubasis_take :: "nat \<Rightarrow> ubasis \<Rightarrow> ubasis"
   10.12 @@ -338,7 +338,7 @@
   10.13  by (rule udom.completion_approx_eq_principal)
   10.14  
   10.15  
   10.16 -subsection {* Universality of @{typ udom} *}
   10.17 +subsection {* Universality of \emph{udom} *}
   10.18  
   10.19  defaultsort bifinite
   10.20  
   10.21 @@ -816,7 +816,7 @@
   10.22    place
   10.23    sub
   10.24  
   10.25 -subsubsection {* EP-pair from any bifinite domain into @{typ udom} *}
   10.26 +subsubsection {* EP-pair from any bifinite domain into \emph{udom} *}
   10.27  
   10.28  definition
   10.29    udom_emb :: "'a::bifinite \<rightarrow> udom"
    11.1 --- a/src/HOLCF/Up.thy	Mon Mar 22 19:29:11 2010 +0100
    11.2 +++ b/src/HOLCF/Up.thy	Mon Mar 22 12:52:51 2010 -0700
    11.3 @@ -169,7 +169,7 @@
    11.4  lemma inst_up_pcpo: "\<bottom> = Ibottom"
    11.5  by (rule minimal_up [THEN UU_I, symmetric])
    11.6  
    11.7 -subsection {* Continuity of @{term Iup} and @{term Ifup} *}
    11.8 +subsection {* Continuity of \emph{Iup} and \emph{Ifup} *}
    11.9  
   11.10  text {* continuity for @{term Iup} *}
   11.11