--- 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"