| changeset 7521 | a18adacbdbd2 |
| parent 6825 | 30e09714eef5 |
| child 7878 | 43b03d412b82 |
--- a/src/HOL/UNITY/LessThan.ML Wed Sep 08 15:44:11 1999 +0200 +++ b/src/HOL/UNITY/LessThan.ML Wed Sep 08 15:44:56 1999 +0200 @@ -43,6 +43,10 @@ by (Blast_tac 1); qed "Compl_lessThan"; +Goal "{k} - lessThan k = {k}"; +by (Blast_tac 1); +qed "single_Diff_lessThan"; +Addsimps [single_Diff_lessThan]; (*** greaterThan ***)