# HG changeset patch
# User krauss
# Date 1211555964 -7200
# Node ID cf147f69b3df90de0b9d8ab6d54e91ef8d857b16
# Parent  103dca19ef2ee8aa2fa8106ca0d84c67e06e8efe
rearranged subsections

diff -r 103dca19ef2e -r cf147f69b3df src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Fri May 23 16:41:39 2008 +0200
+++ b/src/HOL/Wellfounded.thy	Fri May 23 17:19:24 2008 +0200
@@ -12,6 +12,8 @@
 uses ("Tools/function_package/size.ML")
 begin
 
+subsection {* Basic Definitions *}
+
 inductive
   wfrec_rel :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b => bool"
   for R :: "('a * 'a) set"
@@ -88,6 +90,8 @@
 (* [| wf r;  (a,a) ~: r ==> PROP W |] ==> PROP W *)
 lemmas wf_irrefl = wf_not_refl [elim_format]
 
+subsection {* Basic Results *}
+
 text{*transitive closure of a well-founded relation is well-founded! *}
 lemma wf_trancl:
   assumes "wf r"
@@ -129,8 +133,6 @@
   done
 
 
-subsubsection {* Other simple well-foundedness results *}
-
 text{*Minimal-element characterization of well-foundedness*}
 lemma wf_eq_minimal: "wf r = (\<forall>Q x. x\<in>Q --> (\<exists>z\<in>Q. \<forall>y. (y,z)\<in>r --> y\<notin>Q))"
 proof (intro iffI strip)
@@ -222,7 +224,7 @@
 done
 
 
-subsubsection {* Well-Foundedness Results for Unions *}
+subsection {* Well-Foundedness Results for Unions *}
 
 lemma wf_union_compatible:
   assumes "wf R" "wf S"