# HG changeset patch
# User paulson
# Date 936798296 -7200
# Node ID a18adacbdbd2336d61e6ec2a7038574629475dce
# Parent  65f0cec65fc6a88141cd03e7e72cb238e0b2c911
new theorem single_Diff_lessThan

diff -r 65f0cec65fc6 -r a18adacbdbd2 src/HOL/UNITY/LessThan.ML
--- 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 ***)