fix LaTeX overfull hbox warnings in HOLCF document
authorhuffman
Mon Mar 22 13:27:35 2010 -0700 (2010-03-22)
changeset 3590112f09bf2c77f
parent 35900 aa5dfb03eb1e
child 35902 81608655c69e
child 35909 a4ed7aaa7d03
fix LaTeX overfull hbox warnings in HOLCF document
src/HOLCF/Algebraic.thy
src/HOLCF/CompactBasis.thy
src/HOLCF/ConvexPD.thy
src/HOLCF/Deflation.thy
src/HOLCF/LowerPD.thy
src/HOLCF/Representable.thy
src/HOLCF/UpperPD.thy
src/HOLCF/document/root.tex
     1.1 --- a/src/HOLCF/Algebraic.thy	Mon Mar 22 12:52:51 2010 -0700
     1.2 +++ b/src/HOLCF/Algebraic.thy	Mon Mar 22 13:27:35 2010 -0700
     1.3 @@ -714,7 +714,8 @@
     1.4  apply (rule finite_deflation_approx)
     1.5  apply (rule chainE)
     1.6  apply (rule chain_approx)
     1.7 -apply (simp add: cast_alg_defl_principal Abs_fin_defl_inverse finite_deflation_approx)
     1.8 +apply (simp add: cast_alg_defl_principal
     1.9 +  Abs_fin_defl_inverse finite_deflation_approx)
    1.10  done
    1.11  
    1.12  subsection {* Bifinite domains and algebraic deflations *}
     2.1 --- a/src/HOLCF/CompactBasis.thy	Mon Mar 22 12:52:51 2010 -0700
     2.2 +++ b/src/HOLCF/CompactBasis.thy	Mon Mar 22 13:27:35 2010 -0700
     2.3 @@ -217,7 +217,8 @@
     2.4  apply (cut_tac a=x in PDUnit)
     2.5  apply (simp add: PDUnit_def)
     2.6  apply (drule_tac a=x in PDPlus)
     2.7 -apply (simp add: PDUnit_def PDPlus_def Abs_pd_basis_inverse [unfolded pd_basis_def])
     2.8 +apply (simp add: PDUnit_def PDPlus_def
     2.9 +  Abs_pd_basis_inverse [unfolded pd_basis_def])
    2.10  done
    2.11  
    2.12  lemma pd_basis_induct:
    2.13 @@ -245,7 +246,8 @@
    2.14    shows "fold_pd g f (PDPlus t u) = f (fold_pd g f t) (fold_pd g f u)"
    2.15  proof -
    2.16    interpret ab_semigroup_idem_mult f by fact
    2.17 -  show ?thesis unfolding fold_pd_def Rep_PDPlus by (simp add: image_Un fold1_Un2)
    2.18 +  show ?thesis unfolding fold_pd_def Rep_PDPlus
    2.19 +    by (simp add: image_Un fold1_Un2)
    2.20  qed
    2.21  
    2.22  text {* Take function for powerdomain basis *}
     3.1 --- a/src/HOLCF/ConvexPD.thy	Mon Mar 22 12:52:51 2010 -0700
     3.2 +++ b/src/HOLCF/ConvexPD.thy	Mon Mar 22 13:27:35 2010 -0700
     3.3 @@ -517,16 +517,19 @@
     3.4  lemma convex_map_approx: "convex_map\<cdot>(approx n)\<cdot>xs = approx n\<cdot>xs"
     3.5  by (induct xs rule: convex_pd_induct, simp_all)
     3.6  
     3.7 -lemma ep_pair_convex_map: "ep_pair e p \<Longrightarrow> ep_pair (convex_map\<cdot>e) (convex_map\<cdot>p)"
     3.8 +lemma ep_pair_convex_map:
     3.9 +  "ep_pair e p \<Longrightarrow> ep_pair (convex_map\<cdot>e) (convex_map\<cdot>p)"
    3.10  apply default
    3.11  apply (induct_tac x rule: convex_pd_induct, simp_all add: ep_pair.e_inverse)
    3.12 -apply (induct_tac y rule: convex_pd_induct, simp_all add: ep_pair.e_p_below monofun_cfun)
    3.13 +apply (induct_tac y rule: convex_pd_induct)
    3.14 +apply (simp_all add: ep_pair.e_p_below monofun_cfun)
    3.15  done
    3.16  
    3.17  lemma deflation_convex_map: "deflation d \<Longrightarrow> deflation (convex_map\<cdot>d)"
    3.18  apply default
    3.19  apply (induct_tac x rule: convex_pd_induct, simp_all add: deflation.idem)
    3.20 -apply (induct_tac x rule: convex_pd_induct, simp_all add: deflation.below monofun_cfun)
    3.21 +apply (induct_tac x rule: convex_pd_induct)
    3.22 +apply (simp_all add: deflation.below monofun_cfun)
    3.23  done
    3.24  
    3.25  
     4.1 --- a/src/HOLCF/Deflation.thy	Mon Mar 22 12:52:51 2010 -0700
     4.2 +++ b/src/HOLCF/Deflation.thy	Mon Mar 22 13:27:35 2010 -0700
     4.3 @@ -2,7 +2,7 @@
     4.4      Author:     Brian Huffman
     4.5  *)
     4.6  
     4.7 -header {* Continuous deflations and embedding-projection pairs *}
     4.8 +header {* Continuous deflations and ep-pairs *}
     4.9  
    4.10  theory Deflation
    4.11  imports Cfun
     5.1 --- a/src/HOLCF/LowerPD.thy	Mon Mar 22 12:52:51 2010 -0700
     5.2 +++ b/src/HOLCF/LowerPD.thy	Mon Mar 22 13:27:35 2010 -0700
     5.3 @@ -498,13 +498,15 @@
     5.4  lemma ep_pair_lower_map: "ep_pair e p \<Longrightarrow> ep_pair (lower_map\<cdot>e) (lower_map\<cdot>p)"
     5.5  apply default
     5.6  apply (induct_tac x rule: lower_pd_induct, simp_all add: ep_pair.e_inverse)
     5.7 -apply (induct_tac y rule: lower_pd_induct, simp_all add: ep_pair.e_p_below monofun_cfun)
     5.8 +apply (induct_tac y rule: lower_pd_induct)
     5.9 +apply (simp_all add: ep_pair.e_p_below monofun_cfun)
    5.10  done
    5.11  
    5.12  lemma deflation_lower_map: "deflation d \<Longrightarrow> deflation (lower_map\<cdot>d)"
    5.13  apply default
    5.14  apply (induct_tac x rule: lower_pd_induct, simp_all add: deflation.idem)
    5.15 -apply (induct_tac x rule: lower_pd_induct, simp_all add: deflation.below monofun_cfun)
    5.16 +apply (induct_tac x rule: lower_pd_induct)
    5.17 +apply (simp_all add: deflation.below monofun_cfun)
    5.18  done
    5.19  
    5.20  end
     6.1 --- a/src/HOLCF/Representable.thy	Mon Mar 22 12:52:51 2010 -0700
     6.2 +++ b/src/HOLCF/Representable.thy	Mon Mar 22 13:27:35 2010 -0700
     6.3 @@ -517,7 +517,8 @@
     6.4  lemma cast_TypeRep_fun2:
     6.5    assumes f: "\<And>a b. finite_deflation a \<Longrightarrow> finite_deflation b \<Longrightarrow>
     6.6                  finite_deflation (f\<cdot>a\<cdot>b)"
     6.7 -  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"
     6.8 +  shows "cast\<cdot>(TypeRep_fun2 f\<cdot>A\<cdot>B) =
     6.9 +    udom_emb oo f\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj"
    6.10  proof -
    6.11    have 1: "\<And>a b. finite_deflation
    6.12             (udom_emb oo f\<cdot>(Rep_fin_defl a)\<cdot>(Rep_fin_defl b) oo udom_prj)"
     7.1 --- a/src/HOLCF/UpperPD.thy	Mon Mar 22 12:52:51 2010 -0700
     7.2 +++ b/src/HOLCF/UpperPD.thy	Mon Mar 22 13:27:35 2010 -0700
     7.3 @@ -493,13 +493,15 @@
     7.4  lemma ep_pair_upper_map: "ep_pair e p \<Longrightarrow> ep_pair (upper_map\<cdot>e) (upper_map\<cdot>p)"
     7.5  apply default
     7.6  apply (induct_tac x rule: upper_pd_induct, simp_all add: ep_pair.e_inverse)
     7.7 -apply (induct_tac y rule: upper_pd_induct, simp_all add: ep_pair.e_p_below monofun_cfun)
     7.8 +apply (induct_tac y rule: upper_pd_induct)
     7.9 +apply (simp_all add: ep_pair.e_p_below monofun_cfun)
    7.10  done
    7.11  
    7.12  lemma deflation_upper_map: "deflation d \<Longrightarrow> deflation (upper_map\<cdot>d)"
    7.13  apply default
    7.14  apply (induct_tac x rule: upper_pd_induct, simp_all add: deflation.idem)
    7.15 -apply (induct_tac x rule: upper_pd_induct, simp_all add: deflation.below monofun_cfun)
    7.16 +apply (induct_tac x rule: upper_pd_induct)
    7.17 +apply (simp_all add: deflation.below monofun_cfun)
    7.18  done
    7.19  
    7.20  end
     8.1 --- a/src/HOLCF/document/root.tex	Mon Mar 22 12:52:51 2010 -0700
     8.2 +++ b/src/HOLCF/document/root.tex	Mon Mar 22 13:27:35 2010 -0700
     8.3 @@ -21,7 +21,7 @@
     8.4  \tableofcontents
     8.5  
     8.6  \begin{center}
     8.7 -  \includegraphics[scale=0.5]{session_graph}
     8.8 +  \includegraphics[scale=0.45]{session_graph}
     8.9  \end{center}
    8.10  
    8.11  \newpage