proper header and subsection headings
authorhuffman
Mon Feb 22 21:48:20 2010 -0800 (2010-02-22)
changeset 352940e1adc24722f
parent 35293 06a98796453e
child 35307 8ee07543409f
child 35343 523124691b3a
proper header and subsection headings
src/HOL/Quotient.thy
     1.1 --- a/src/HOL/Quotient.thy	Mon Feb 22 21:47:21 2010 -0800
     1.2 +++ b/src/HOL/Quotient.thy	Mon Feb 22 21:48:20 2010 -0800
     1.3 @@ -2,6 +2,8 @@
     1.4      Author:     Cezary Kaliszyk and Christian Urban
     1.5  *)
     1.6  
     1.7 +header {* Definition of Quotient Types *}
     1.8 +
     1.9  theory Quotient
    1.10  imports Plain ATP_Linkup
    1.11  uses
    1.12 @@ -80,7 +82,7 @@
    1.13    shows "((op =) OOO R) = R"
    1.14    by (auto simp add: expand_fun_eq)
    1.15  
    1.16 -section {* Respects predicate *}
    1.17 +subsection {* Respects predicate *}
    1.18  
    1.19  definition
    1.20    Respects
    1.21 @@ -92,7 +94,7 @@
    1.22    unfolding mem_def Respects_def
    1.23    by simp
    1.24  
    1.25 -section {* Function map and function relation *}
    1.26 +subsection {* Function map and function relation *}
    1.27  
    1.28  definition
    1.29    fun_map (infixr "--->" 55)
    1.30 @@ -124,7 +126,7 @@
    1.31    using a by auto
    1.32  
    1.33  
    1.34 -section {* Quotient Predicate *}
    1.35 +subsection {* Quotient Predicate *}
    1.36  
    1.37  definition
    1.38    "Quotient E Abs Rep \<equiv>
    1.39 @@ -285,7 +287,7 @@
    1.40    shows "R2 (f x) (g y)"
    1.41    using a by simp
    1.42  
    1.43 -section {* lemmas for regularisation of ball and bex *}
    1.44 +subsection {* lemmas for regularisation of ball and bex *}
    1.45  
    1.46  lemma ball_reg_eqv:
    1.47    fixes P :: "'a \<Rightarrow> bool"
    1.48 @@ -387,7 +389,7 @@
    1.49    shows "(\<exists>x. \<exists>y. A x y) \<longrightarrow> (\<exists>x\<in>P. \<exists>y. B x y)"
    1.50    using assms by auto
    1.51  
    1.52 -section {* Bounded abstraction *}
    1.53 +subsection {* Bounded abstraction *}
    1.54  
    1.55  definition
    1.56    Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
    1.57 @@ -465,7 +467,7 @@
    1.58    using a unfolding Quotient_def Bex_def in_respects fun_map_def id_apply
    1.59    by metis
    1.60  
    1.61 -section {* @{text Bex1_rel} quantifier *}
    1.62 +subsection {* @{text Bex1_rel} quantifier *}
    1.63  
    1.64  definition
    1.65    Bex1_rel :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
    1.66 @@ -569,7 +571,7 @@
    1.67    apply auto
    1.68    done
    1.69  
    1.70 -section {* Various respects and preserve lemmas *}
    1.71 +subsection {* Various respects and preserve lemmas *}
    1.72  
    1.73  lemma quot_rel_rsp:
    1.74    assumes a: "Quotient R Abs Rep"
    1.75 @@ -706,7 +708,7 @@
    1.76  
    1.77  end
    1.78  
    1.79 -section {* ML setup *}
    1.80 +subsection {* ML setup *}
    1.81  
    1.82  text {* Auxiliary data for the quotient package *}
    1.83  
    1.84 @@ -762,7 +764,7 @@
    1.85  text {* Tactics for proving the lifted theorems *}
    1.86  use "~~/src/HOL/Tools/Quotient/quotient_tacs.ML"
    1.87  
    1.88 -section {* Methods / Interface *}
    1.89 +subsection {* Methods / Interface *}
    1.90  
    1.91  method_setup lifting =
    1.92    {* Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.lift_tac ctxt thms))) *}