# HG changeset patch
# User huffman
# Date 1269287571 25200
# Node ID aa5dfb03eb1ed6f34c006a378f60a16b300e43cc
# Parent  8758895ea4136b0cdae6496c53a605740ca194f3
remove LaTeX hyperref warnings by avoiding antiquotations within section headings

diff -r 8758895ea413 -r aa5dfb03eb1e src/HOLCF/Cont.thy
--- 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 *}
 
diff -r 8758895ea413 -r aa5dfb03eb1e src/HOLCF/Cprod.thy
--- 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
diff -r 8758895ea413 -r aa5dfb03eb1e src/HOLCF/Discrete.thy
--- 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
diff -r 8758895ea413 -r aa5dfb03eb1e src/HOLCF/Pcpodef.thy
--- 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
diff -r 8758895ea413 -r aa5dfb03eb1e src/HOLCF/Product_Cpo.thy
--- 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)
diff -r 8758895ea413 -r aa5dfb03eb1e src/HOLCF/Representable.thy
--- 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 *}
 
diff -r 8758895ea413 -r aa5dfb03eb1e src/HOLCF/Sprod.thy
--- 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)
diff -r 8758895ea413 -r aa5dfb03eb1e src/HOLCF/Ssum.thy
--- 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 *}
 
diff -r 8758895ea413 -r aa5dfb03eb1e src/HOLCF/Sum_Cpo.thy
--- 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)
diff -r 8758895ea413 -r aa5dfb03eb1e src/HOLCF/Universal.thy
--- 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"
diff -r 8758895ea413 -r aa5dfb03eb1e src/HOLCF/Up.thy
--- 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} *}