equal
deleted
inserted
replaced
304 "irrefl r \<longleftrightarrow> (\<forall>(x, y) \<in> r. x \<noteq> y)" |
304 "irrefl r \<longleftrightarrow> (\<forall>(x, y) \<in> r. x \<noteq> y)" |
305 by (auto simp add: irrefl_def) |
305 by (auto simp add: irrefl_def) |
306 |
306 |
307 lemma irrefl_diff_Id[simp]: "irrefl(r-Id)" |
307 lemma irrefl_diff_Id[simp]: "irrefl(r-Id)" |
308 by(simp add:irrefl_def) |
308 by(simp add:irrefl_def) |
|
309 |
309 |
310 |
310 subsection {* Totality *} |
311 subsection {* Totality *} |
311 |
312 |
312 lemma total_on_empty[simp]: "total_on {} r" |
313 lemma total_on_empty[simp]: "total_on {} r" |
313 by(simp add:total_on_def) |
314 by(simp add:total_on_def) |