fix LaTeX overfull hbox warnings in HOLCF document

--- a/src/HOLCF/Algebraic.thy	Mon Mar 22 12:52:51 2010 -0700
+++ b/src/HOLCF/Algebraic.thy	Mon Mar 22 13:27:35 2010 -0700
@@ -714,7 +714,8 @@
 apply (rule finite_deflation_approx)
 apply (rule chainE)
 apply (rule chain_approx)
-apply (simp add: cast_alg_defl_principal Abs_fin_defl_inverse finite_deflation_approx)
+apply (simp add: cast_alg_defl_principal
+  Abs_fin_defl_inverse finite_deflation_approx)
 done
 
 subsection {* Bifinite domains and algebraic deflations *}

--- a/src/HOLCF/CompactBasis.thy	Mon Mar 22 12:52:51 2010 -0700
+++ b/src/HOLCF/CompactBasis.thy	Mon Mar 22 13:27:35 2010 -0700
@@ -217,7 +217,8 @@
 apply (cut_tac a=x in PDUnit)
 apply (simp add: PDUnit_def)
 apply (drule_tac a=x in PDPlus)
-apply (simp add: PDUnit_def PDPlus_def Abs_pd_basis_inverse [unfolded pd_basis_def])
+apply (simp add: PDUnit_def PDPlus_def
+  Abs_pd_basis_inverse [unfolded pd_basis_def])
 done
 
 lemma pd_basis_induct:
@@ -245,7 +246,8 @@
   shows "fold_pd g f (PDPlus t u) = f (fold_pd g f t) (fold_pd g f u)"
 proof -
   interpret ab_semigroup_idem_mult f by fact
-  show ?thesis unfolding fold_pd_def Rep_PDPlus by (simp add: image_Un fold1_Un2)
+  show ?thesis unfolding fold_pd_def Rep_PDPlus
+    by (simp add: image_Un fold1_Un2)
 qed
 
 text {* Take function for powerdomain basis *}

--- a/src/HOLCF/ConvexPD.thy	Mon Mar 22 12:52:51 2010 -0700
+++ b/src/HOLCF/ConvexPD.thy	Mon Mar 22 13:27:35 2010 -0700
@@ -517,16 +517,19 @@
 lemma convex_map_approx: "convex_map\<cdot>(approx n)\<cdot>xs = approx n\<cdot>xs"
 by (induct xs rule: convex_pd_induct, simp_all)
 
-lemma ep_pair_convex_map: "ep_pair e p \<Longrightarrow> ep_pair (convex_map\<cdot>e) (convex_map\<cdot>p)"
+lemma ep_pair_convex_map:
+  "ep_pair e p \<Longrightarrow> ep_pair (convex_map\<cdot>e) (convex_map\<cdot>p)"
 apply default
 apply (induct_tac x rule: convex_pd_induct, simp_all add: ep_pair.e_inverse)
-apply (induct_tac y rule: convex_pd_induct, simp_all add: ep_pair.e_p_below monofun_cfun)
+apply (induct_tac y rule: convex_pd_induct)
+apply (simp_all add: ep_pair.e_p_below monofun_cfun)
 done
 
 lemma deflation_convex_map: "deflation d \<Longrightarrow> deflation (convex_map\<cdot>d)"
 apply default
 apply (induct_tac x rule: convex_pd_induct, simp_all add: deflation.idem)
-apply (induct_tac x rule: convex_pd_induct, simp_all add: deflation.below monofun_cfun)
+apply (induct_tac x rule: convex_pd_induct)
+apply (simp_all add: deflation.below monofun_cfun)
 done
 
 

--- a/src/HOLCF/Deflation.thy	Mon Mar 22 12:52:51 2010 -0700
+++ b/src/HOLCF/Deflation.thy	Mon Mar 22 13:27:35 2010 -0700
@@ -2,7 +2,7 @@
     Author:     Brian Huffman
 *)
 
-header {* Continuous deflations and embedding-projection pairs *}
+header {* Continuous deflations and ep-pairs *}
 
 theory Deflation
 imports Cfun

--- a/src/HOLCF/LowerPD.thy	Mon Mar 22 12:52:51 2010 -0700
+++ b/src/HOLCF/LowerPD.thy	Mon Mar 22 13:27:35 2010 -0700
@@ -498,13 +498,15 @@
 lemma ep_pair_lower_map: "ep_pair e p \<Longrightarrow> ep_pair (lower_map\<cdot>e) (lower_map\<cdot>p)"
 apply default
 apply (induct_tac x rule: lower_pd_induct, simp_all add: ep_pair.e_inverse)
-apply (induct_tac y rule: lower_pd_induct, simp_all add: ep_pair.e_p_below monofun_cfun)
+apply (induct_tac y rule: lower_pd_induct)
+apply (simp_all add: ep_pair.e_p_below monofun_cfun)
 done
 
 lemma deflation_lower_map: "deflation d \<Longrightarrow> deflation (lower_map\<cdot>d)"
 apply default
 apply (induct_tac x rule: lower_pd_induct, simp_all add: deflation.idem)
-apply (induct_tac x rule: lower_pd_induct, simp_all add: deflation.below monofun_cfun)
+apply (induct_tac x rule: lower_pd_induct)
+apply (simp_all add: deflation.below monofun_cfun)
 done
 
 end

--- a/src/HOLCF/Representable.thy	Mon Mar 22 12:52:51 2010 -0700
+++ b/src/HOLCF/Representable.thy	Mon Mar 22 13:27:35 2010 -0700
@@ -517,7 +517,8 @@
 lemma cast_TypeRep_fun2:
   assumes f: "\<And>a b. finite_deflation a \<Longrightarrow> finite_deflation b \<Longrightarrow>
                 finite_deflation (f\<cdot>a\<cdot>b)"
-  shows "cast\<cdot>(TypeRep_fun2 f\<cdot>A\<cdot>B) = udom_emb oo f\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj"
+  shows "cast\<cdot>(TypeRep_fun2 f\<cdot>A\<cdot>B) =
+    udom_emb oo f\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj"
 proof -
   have 1: "\<And>a b. finite_deflation
            (udom_emb oo f\<cdot>(Rep_fin_defl a)\<cdot>(Rep_fin_defl b) oo udom_prj)"

--- a/src/HOLCF/UpperPD.thy	Mon Mar 22 12:52:51 2010 -0700
+++ b/src/HOLCF/UpperPD.thy	Mon Mar 22 13:27:35 2010 -0700
@@ -493,13 +493,15 @@
 lemma ep_pair_upper_map: "ep_pair e p \<Longrightarrow> ep_pair (upper_map\<cdot>e) (upper_map\<cdot>p)"
 apply default
 apply (induct_tac x rule: upper_pd_induct, simp_all add: ep_pair.e_inverse)
-apply (induct_tac y rule: upper_pd_induct, simp_all add: ep_pair.e_p_below monofun_cfun)
+apply (induct_tac y rule: upper_pd_induct)
+apply (simp_all add: ep_pair.e_p_below monofun_cfun)
 done
 
 lemma deflation_upper_map: "deflation d \<Longrightarrow> deflation (upper_map\<cdot>d)"
 apply default
 apply (induct_tac x rule: upper_pd_induct, simp_all add: deflation.idem)
-apply (induct_tac x rule: upper_pd_induct, simp_all add: deflation.below monofun_cfun)
+apply (induct_tac x rule: upper_pd_induct)
+apply (simp_all add: deflation.below monofun_cfun)
 done
 
 end

--- a/src/HOLCF/document/root.tex	Mon Mar 22 12:52:51 2010 -0700
+++ b/src/HOLCF/document/root.tex	Mon Mar 22 13:27:35 2010 -0700
@@ -21,7 +21,7 @@
 \tableofcontents
 
 \begin{center}
-  \includegraphics[scale=0.5]{session_graph}
+  \includegraphics[scale=0.45]{session_graph}
 \end{center}
 
 \newpage