--- a/src/HOL/ex/set.ML Mon Feb 21 10:20:38 2000 +0100
+++ b/src/HOL/ex/set.ML Mon Feb 21 11:15:43 2000 +0100
@@ -11,6 +11,17 @@
context Lfp.thy;
+(*These two are cited in Benzmueller and Kohlhash's system description of LEO,
+ CADE-15, 1998 (page 139-143) as theorems LEO could not prove.*)
+
+Goal "(X = Y Un Z) = (Y<=X & Z<=X & (ALL V. Y<=V & Z<=V --> X<=V))";
+by (Blast_tac 1);
+result();
+
+Goal "(X = Y Int Z) = (X<=Y & X<=Z & (ALL V. V<=Y & V<=Z --> V<=X))";
+by (Blast_tac 1);
+result();
+
(*trivial example of term synthesis: apparently hard for some provers!*)
Goal "a ~= b ==> a:?X & b ~: ?X";
by (Blast_tac 1);
--- a/src/ZF/ex/misc.ML Mon Feb 21 10:20:38 2000 +0100
+++ b/src/ZF/ex/misc.ML Mon Feb 21 11:15:43 2000 +0100
@@ -9,6 +9,18 @@
writeln"ZF/ex/misc";
+(*These two are cited in Benzmueller and Kohlhash's system description of LEO,
+ CADE-15, 1998 (page 139-143) as theorems LEO could not prove.*)
+
+Goal "(X = Y Un Z) <-> (Y<=X & Z<=X & (ALL V. Y<=V & Z<=V --> X<=V))";
+by (blast_tac (claset() addSIs [equalityI]) 1);
+result();
+
+(*the dual of the previous one*)
+Goal "(X = Y Int Z) <-> (X<=Y & X<=Z & (ALL V. V<=Y & V<=Z --> V<=X))";
+by (blast_tac (claset() addSIs [equalityI]) 1);
+result();
+
(*trivial example of term synthesis: apparently hard for some provers!*)
Goal "a ~= b ==> a:?X & b ~: ?X";
by (Blast_tac 1);