# HG changeset patch
# User paulson
# Date 959260554 -7200
# Node ID bcd34d580839e6c093e31707902a40519a21b2c0
# Parent  a76f80911eb9d36cd9c1871fe435e8ed9b45f7da
moved mostly to HOL/SetInterval.ML and UNITY/UNITY.ML

diff -r a76f80911eb9 -r bcd34d580839 src/HOL/UNITY/LessThan.ML
--- a/src/HOL/UNITY/LessThan.ML	Thu May 25 15:15:22 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,47 +0,0 @@
-(*  Title:      HOL/LessThan/LessThan
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1998  University of Cambridge
-
-*)
-
-
-(*** Finally, a few set-theoretic laws...
-     CAN BOOLEAN SIMPLIFICATION BE AUTOMATED? ***)
-
-(** Rewrite rules to eliminate A.  Conditions can be satisfied by letting B
-    be any set including A Int C and contained in A Un C, such as B=A or B=C.
-**)
-
-Goal "[| A Int C <= B; B <= A Un C |] \
-\     ==> (A Int B) Un (-A Int C) = B Un C";
-by (Blast_tac 1);
-qed "set_cancel1";
-
-Goal "[| A Int C <= B; B <= A Un C |] \
-\     ==> (A Un B) Int (-A Un C) = B Int C";
-by (Blast_tac 1);
-qed "set_cancel2";
-
-(*The base B=A*)
-Goal "A Un (-A Int C) = A Un C";
-by (Blast_tac 1);
-qed "set_cancel3";
-
-Goal "A Int (-A Un C) = A Int C";
-by (Blast_tac 1);
-qed "set_cancel4";
-
-(*The base B=C*)
-Goal "(A Int C) Un (-A Int C) = C";
-by (Blast_tac 1);
-qed "set_cancel5";
-
-Goal "(A Un C) Int (-A Un C) = C";
-by (Blast_tac 1);
-qed "set_cancel6";
-
-Addsimps [set_cancel1, set_cancel2, set_cancel3,
-	  set_cancel4, set_cancel5, set_cancel6];
-
-