remove LaTeX hyperref warnings by avoiding antiquotations within section headings
--- a/src/HOLCF/Cont.thy Mon Mar 22 19:29:11 2010 +0100
+++ b/src/HOLCF/Cont.thy Mon Mar 22 12:52:51 2010 -0700
@@ -55,7 +55,7 @@
by (simp add: monofun_def)
-subsection {* @{prop "monofun f \<and> contlub f \<equiv> cont f"} *}
+subsection {* Equivalence of alternate definition *}
text {* monotone functions map chains to chains *}
--- a/src/HOLCF/Cprod.thy Mon Mar 22 19:29:11 2010 +0100
+++ b/src/HOLCF/Cprod.thy Mon Mar 22 12:52:51 2010 -0700
@@ -10,7 +10,7 @@
defaultsort cpo
-subsection {* Type @{typ unit} is a pcpo *}
+subsection {* Continuous case function for unit type *}
definition
unit_when :: "'a \<rightarrow> unit \<rightarrow> 'a" where
--- a/src/HOLCF/Discrete.thy Mon Mar 22 19:29:11 2010 +0100
+++ b/src/HOLCF/Discrete.thy Mon Mar 22 12:52:51 2010 -0700
@@ -10,7 +10,7 @@
datatype 'a discr = Discr "'a :: type"
-subsection {* Type @{typ "'a discr"} is a discrete cpo *}
+subsection {* Discrete ordering *}
instantiation discr :: (type) below
begin
@@ -22,14 +22,14 @@
instance ..
end
+subsection {* Discrete cpo class instance *}
+
instance discr :: (type) discrete_cpo
by intro_classes (simp add: below_discr_def)
lemma discr_below_eq [iff]: "((x::('a::type)discr) << y) = (x = y)"
by simp (* FIXME: same discrete_cpo - remove? is [iff] important? *)
-subsection {* Type @{typ "'a discr"} is a cpo *}
-
lemma discr_chain0:
"!!S::nat=>('a::type)discr. chain S ==> S i = S 0"
apply (unfold chain_def)
@@ -60,7 +60,7 @@
apply (clarify, erule discr_chain0 [symmetric])
done
-subsection {* @{term undiscr} *}
+subsection {* \emph{undiscr} *}
definition
undiscr :: "('a::type)discr => 'a" where
--- a/src/HOLCF/Pcpodef.thy Mon Mar 22 19:29:11 2010 +0100
+++ b/src/HOLCF/Pcpodef.thy Mon Mar 22 12:52:51 2010 -0700
@@ -129,7 +129,7 @@
thus "\<exists>x. range S <<| x" ..
qed
-subsubsection {* Continuity of @{term Rep} and @{term Abs} *}
+subsubsection {* Continuity of \emph{Rep} and \emph{Abs} *}
text {* For any sub-cpo, the @{term Rep} function is continuous. *}
@@ -229,7 +229,7 @@
shows "OFCLASS('b, pcpo_class)"
by (rule typedef_pcpo_generic [OF type below UU_in_A], rule minimal)
-subsubsection {* Strictness of @{term Rep} and @{term Abs} *}
+subsubsection {* Strictness of \emph{Rep} and \emph{Abs} *}
text {*
For a sub-pcpo where @{term \<bottom>} is a member of the defining
--- a/src/HOLCF/Product_Cpo.thy Mon Mar 22 19:29:11 2010 +0100
+++ b/src/HOLCF/Product_Cpo.thy Mon Mar 22 12:52:51 2010 -0700
@@ -10,7 +10,7 @@
defaultsort cpo
-subsection {* Type @{typ unit} is a pcpo *}
+subsection {* Unit type is a pcpo *}
instantiation unit :: below
begin
@@ -58,7 +58,7 @@
by (fast intro: below_trans)
qed
-subsection {* Monotonicity of @{text "(_,_)"}, @{term fst}, @{term snd} *}
+subsection {* Monotonicity of \emph{Pair}, \emph{fst}, \emph{snd} *}
lemma prod_belowI: "\<lbrakk>fst p \<sqsubseteq> fst q; snd p \<sqsubseteq> snd q\<rbrakk> \<Longrightarrow> p \<sqsubseteq> q"
unfolding below_prod_def by simp
@@ -187,7 +187,7 @@
lemma split_strict [simp]: "split f \<bottom> = f \<bottom> \<bottom>"
unfolding split_def by simp
-subsection {* Continuity of @{text "(_,_)"}, @{term fst}, @{term snd} *}
+subsection {* Continuity of \emph{Pair}, \emph{fst}, \emph{snd} *}
lemma cont_pair1: "cont (\<lambda>x. (x, y))"
apply (rule contI)
--- a/src/HOLCF/Representable.thy Mon Mar 22 19:29:11 2010 +0100
+++ b/src/HOLCF/Representable.thy Mon Mar 22 12:52:51 2010 -0700
@@ -35,7 +35,7 @@
lemmas prj_strict = rep.p_strict
-subsection {* Making @{term rep} the default class *}
+subsection {* Making \emph{rep} the default class *}
text {*
From now on, free type variables are assumed to be in class
@@ -342,7 +342,7 @@
use "Tools/repdef.ML"
-subsection {* Instances of class @{text rep} *}
+subsection {* Instances of class \emph{rep} *}
subsubsection {* Universal Domain *}
--- a/src/HOLCF/Sprod.thy Mon Mar 22 19:29:11 2010 +0100
+++ b/src/HOLCF/Sprod.thy Mon Mar 22 12:52:51 2010 -0700
@@ -88,7 +88,7 @@
"\<lbrakk>P \<bottom>; \<And>x y. \<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> P (:x, y:)\<rbrakk> \<Longrightarrow> P x"
by (cases x, simp_all)
-subsection {* Properties of @{term spair} *}
+subsection {* Properties of \emph{spair} *}
lemma spair_strict1 [simp]: "(:\<bottom>, y:) = \<bottom>"
by (simp add: Rep_Sprod_simps strictify_conv_if)
@@ -134,7 +134,7 @@
lemma sprodE2: "(\<And>x y. p = (:x, y:) \<Longrightarrow> Q) \<Longrightarrow> Q"
by (cases p, simp only: inst_sprod_pcpo2, simp)
-subsection {* Properties of @{term sfst} and @{term ssnd} *}
+subsection {* Properties of \emph{sfst} and \emph{ssnd} *}
lemma sfst_strict [simp]: "sfst\<cdot>\<bottom> = \<bottom>"
by (simp add: sfst_def cont_Rep_Sprod Rep_Sprod_strict)
@@ -208,7 +208,7 @@
apply simp
done
-subsection {* Properties of @{term ssplit} *}
+subsection {* Properties of \emph{ssplit} *}
lemma ssplit1 [simp]: "ssplit\<cdot>f\<cdot>\<bottom> = \<bottom>"
by (simp add: ssplit_def)
--- a/src/HOLCF/Ssum.thy Mon Mar 22 19:29:11 2010 +0100
+++ b/src/HOLCF/Ssum.thy Mon Mar 22 12:52:51 2010 -0700
@@ -58,7 +58,7 @@
lemma Rep_Ssum_sinr: "Rep_Ssum (sinr\<cdot>b) = (strictify\<cdot>(\<Lambda> _. FF)\<cdot>b, \<bottom>, b)"
by (simp add: sinr_Abs_Ssum Abs_Ssum_inverse sinr_Ssum)
-subsection {* Properties of @{term sinl} and @{term sinr} *}
+subsection {* Properties of \emph{sinl} and \emph{sinr} *}
text {* Ordering *}
--- a/src/HOLCF/Sum_Cpo.thy Mon Mar 22 19:29:11 2010 +0100
+++ b/src/HOLCF/Sum_Cpo.thy Mon Mar 22 12:52:51 2010 -0700
@@ -8,7 +8,7 @@
imports Bifinite
begin
-subsection {* Ordering on type @{typ "'a + 'b"} *}
+subsection {* Ordering on sum type *}
instantiation "+" :: (below, below) below
begin
@@ -128,7 +128,7 @@
apply (erule cpo_lubI)
done
-subsection {* Continuity of @{term Inl}, @{term Inr}, @{term sum_case} *}
+subsection {* Continuity of \emph{Inl}, \emph{Inr}, and case function *}
lemma cont_Inl: "cont Inl"
by (intro contI is_lub_Inl cpo_lubI)
--- a/src/HOLCF/Universal.thy Mon Mar 22 19:29:11 2010 +0100
+++ b/src/HOLCF/Universal.thy Mon Mar 22 12:52:51 2010 -0700
@@ -187,7 +187,7 @@
apply simp
done
-subsubsection {* Take function for @{typ ubasis} *}
+subsubsection {* Take function for \emph{ubasis} *}
definition
ubasis_take :: "nat \<Rightarrow> ubasis \<Rightarrow> ubasis"
@@ -338,7 +338,7 @@
by (rule udom.completion_approx_eq_principal)
-subsection {* Universality of @{typ udom} *}
+subsection {* Universality of \emph{udom} *}
defaultsort bifinite
@@ -816,7 +816,7 @@
place
sub
-subsubsection {* EP-pair from any bifinite domain into @{typ udom} *}
+subsubsection {* EP-pair from any bifinite domain into \emph{udom} *}
definition
udom_emb :: "'a::bifinite \<rightarrow> udom"
--- a/src/HOLCF/Up.thy Mon Mar 22 19:29:11 2010 +0100
+++ b/src/HOLCF/Up.thy Mon Mar 22 12:52:51 2010 -0700
@@ -169,7 +169,7 @@
lemma inst_up_pcpo: "\<bottom> = Ibottom"
by (rule minimal_up [THEN UU_I, symmetric])
-subsection {* Continuity of @{term Iup} and @{term Ifup} *}
+subsection {* Continuity of \emph{Iup} and \emph{Ifup} *}
text {* continuity for @{term Iup} *}