# HG changeset patch
# User huffman
# Date 1289443548 28800
# Node ID 4c5363173f8888a3a20bbd513a017827355872d8
# Parent  702708d26c9b6762d557873abe33a040a6aba07f
section headings

diff -r 702708d26c9b -r 4c5363173f88 src/HOLCF/Bifinite.thy
--- a/src/HOLCF/Bifinite.thy	Wed Nov 10 18:37:11 2010 -0800
+++ b/src/HOLCF/Bifinite.thy	Wed Nov 10 18:45:48 2010 -0800
@@ -308,7 +308,9 @@
   , (@{const_name liftprj}, SOME @{typ "udom \<rightarrow> 'a::predomain u"}) ]
 *}
 
-subsection {* The universal domain is a domain *}
+subsection {* Class instance proofs *}
+
+subsubsection {* Universal domain *}
 
 instantiation udom :: liftdomain
 begin
@@ -352,7 +354,7 @@
 
 end
 
-subsection {* Lifted predomains are domains *}
+subsubsection {* Lifted cpo *}
 
 instantiation u :: (predomain) liftdomain
 begin
@@ -391,7 +393,7 @@
 lemma DEFL_u: "DEFL('a::predomain u) = LIFTDEFL('a)"
 by (rule defl_u_def)
 
-subsection {* Continuous function space is a domain *}
+subsubsection {* Continuous function space *}
 
 text {* TODO: Allow argument type to be a predomain. *}
 
@@ -434,7 +436,7 @@
   "DEFL('a::domain \<rightarrow> 'b::domain) = cfun_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
 by (rule defl_cfun_def)
 
-subsection {* Cartesian product is a domain *}
+subsubsection {* Cartesian product *}
 
 text {*
   Types @{typ "('a * 'b) u"} and @{typ "'a u \<otimes> 'b u"} are isomorphic.
@@ -520,7 +522,7 @@
   "LIFTDEFL('a::predomain \<times> 'b::predomain) = sprod_defl\<cdot>DEFL('a u)\<cdot>DEFL('b u)"
 by (rule liftdefl_prod_def)
 
-subsection {* Strict product is a domain *}
+subsubsection {* Strict product *}
 
 instantiation sprod :: ("domain", "domain") liftdomain
 begin
@@ -562,7 +564,7 @@
   "DEFL('a::domain \<otimes> 'b::domain) = sprod_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
 by (rule defl_sprod_def)
 
-subsection {* Countable discrete cpos are predomains *}
+subsubsection {* Discrete cpo *}
 
 definition discr_approx :: "nat \<Rightarrow> 'a::countable discr u \<rightarrow> 'a discr u"
   where "discr_approx = (\<lambda>i. \<Lambda>(up\<cdot>x). if to_nat (undiscr x) < i then up\<cdot>x else \<bottom>)"
@@ -651,7 +653,7 @@
 
 end
 
-subsection {* Strict sum is a domain *}
+subsubsection {* Strict sum *}
 
 instantiation ssum :: ("domain", "domain") liftdomain
 begin
@@ -692,7 +694,7 @@
   "DEFL('a::domain \<oplus> 'b::domain) = ssum_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
 by (rule defl_ssum_def)
 
-subsection {* Lifted countable types are bifinite domains *}
+subsubsection {* Lifted HOL type *}
 
 instantiation lift :: (countable) liftdomain
 begin