| changeset 71827 | 5e315defb038 |
| parent 71766 | 1249b998e377 |
| child 71935 | 82b00b8f1871 |
--- a/src/HOL/Wellfounded.thy Sat May 09 17:20:04 2020 +0000 +++ b/src/HOL/Wellfounded.thy Mon May 11 11:15:41 2020 +0100 @@ -580,6 +580,9 @@ lemma less_than_iff [iff]: "((x,y) \<in> less_than) = (x<y)" by (simp add: less_than_def less_eq) +lemma irrefl_less_than: "irrefl less_than" + using irrefl_def by blast + lemma total_less_than: "total less_than" and total_on_less_than [simp]: "total_on A less_than" using total_on_def by force+