--- a/src/HOL/Relation.thy Thu Oct 13 22:56:19 2011 +0200
+++ b/src/HOL/Relation.thy Thu Oct 13 23:02:59 2011 +0200
@@ -307,6 +307,7 @@
lemma irrefl_diff_Id[simp]: "irrefl(r-Id)"
by(simp add:irrefl_def)
+
subsection {* Totality *}
lemma total_on_empty[simp]: "total_on {} r"