src/HOL/Relation.thy
changeset 45139 bdcaa3f3a2f4
parent 45137 6e422d180de8
child 45967 76cf71ed15c7
     1.1 --- a/src/HOL/Relation.thy	Thu Oct 13 22:56:19 2011 +0200
     1.2 +++ b/src/HOL/Relation.thy	Thu Oct 13 23:02:59 2011 +0200
     1.3 @@ -307,6 +307,7 @@
     1.4  lemma irrefl_diff_Id[simp]: "irrefl(r-Id)"
     1.5  by(simp add:irrefl_def)
     1.6  
     1.7 +
     1.8  subsection {* Totality *}
     1.9  
    1.10  lemma total_on_empty[simp]: "total_on {} r"