# HG changeset patch
# User paulson
# Date 951213073 -3600
# Node ID 9f9e6c65487d517a08c1eda56685812c5871b767
# Parent  1329173b56edc988d981c2852daf748b6532a21c
three easy new examples

diff -r 1329173b56ed -r 9f9e6c65487d src/FOL/ex/int.ML
--- a/src/FOL/ex/int.ML	Mon Feb 21 14:10:21 2000 +0100
+++ b/src/FOL/ex/int.ML	Tue Feb 22 10:51:13 2000 +0100
@@ -35,6 +35,10 @@
 by (IntPr.fast_tac 1);
 result();
 
+Goal "~~ ((~P --> Q) --> (~P --> ~Q) --> P)";
+by (IntPr.fast_tac 1);
+result();
+
 (* ~~ does NOT distribute over | *)
 
 Goal "~~(P-->Q)  <-> (~~P --> ~~Q)";
@@ -53,6 +57,16 @@
 by (IntPr.fast_tac 1);
 result();
 
+Goal "((P --> (Q | (Q-->R))) --> R) --> R";
+by (IntPr.fast_tac 1);
+result();
+
+Goal "(((G-->A) --> J) --> D --> E) --> (((H-->B)-->I)-->C-->J) \
+\     --> (A-->H) --> F --> G --> (((C-->B)-->I)-->D)-->(A-->C) \
+\     --> (((F-->A)-->B) --> I) --> E";
+by (IntPr.fast_tac 1);
+result();
+
 
 writeln"Lemmas for the propositional double-negation translation";
 
@@ -110,7 +124,7 @@
 Goal "(ALL x. EX y. ALL z. p(x) & q(y) & r(z)) <->  \
 \     (ALL z. EX y. ALL x. p(x) & q(y) & r(z))";
 (*
-by (IntPr.best_dup_tac 1);   (*2 minutes!  Is it worth it?*)
+by (IntPr.best_dup_tac 1);   (*65 seconds on a Pentium III!  Is it worth it?*)
 *)
 
 (*Problem 3.1*)