# HG changeset patch
# User lcp
# Date 783620268 -3600
# Node ID c801110efa1ba8b224e2676a8604d0db33d5a911
# Parent  c0ff8f1ebc16ea7b674b30d3104f10edc1711648
HOL/ex/cla: proofs now use deepen_tac instead of best_tac HOL_dup_cs

diff -r c0ff8f1ebc16 -r c801110efa1b ex/cla.ML
--- a/ex/cla.ML	Thu Oct 13 09:39:15 1994 +0100
+++ b/ex/cla.ML	Mon Oct 31 17:17:48 1994 +0100
@@ -1,7 +1,7 @@
 (*  Title: 	HOL/ex/cla
     ID:         $Id$
     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1992  University of Cambridge
+    Copyright   1994  University of Cambridge
 
 Higher-Order Logic: predicate calculus problems
 
@@ -151,32 +151,32 @@
 
 (*Needs multiple instantiation of the quantifier.*)
 goal HOL.thy "(! x. P(x)-->P(f(x)))  &  P(d)-->P(f(f(f(d))))";
-by (best_tac HOL_dup_cs 1);
+by (deepen_tac HOL_cs 1 1);
 result();
 
 (*Needs double instantiation of the quantifier*)
 goal HOL.thy "? x. P(x) --> P(a) & P(b)";
-by (best_tac HOL_dup_cs 1);
+by (deepen_tac HOL_cs 1 1);
 result();
 
 goal HOL.thy "? z. P(z) --> (! x. P(x))";
-by (best_tac HOL_dup_cs 1);
+by (deepen_tac HOL_cs 1 1);
 result();
 
 goal HOL.thy "? x. (? y. P(y)) --> P(x)";
-by (best_tac HOL_dup_cs 1);
+by (deepen_tac HOL_cs 1 1);
 result();
 
 writeln"Hard examples with quantifiers";
 
 writeln"Problem 18";
 goal HOL.thy "? y. ! x. P(y)-->P(x)";
-by (best_tac HOL_dup_cs 1);
+by (deepen_tac HOL_cs 1 1);
 result(); 
 
 writeln"Problem 19";
 goal HOL.thy "? x. ! y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))";
-by (best_tac HOL_dup_cs 1);
+by (deepen_tac HOL_cs 1 1);
 result();
 
 writeln"Problem 20";
@@ -187,7 +187,7 @@
 
 writeln"Problem 21";
 goal HOL.thy "(? x. P-->Q(x)) & (? x. Q(x)-->P) --> (? x. P=Q(x))";
-by (best_tac HOL_dup_cs 1); 
+by (deepen_tac HOL_cs 1 1); 
 result();
 
 writeln"Problem 22";
@@ -282,14 +282,13 @@
 \                   ((? x. q(x)) = (! y. p(y))))   =	\
 \                  ((? x. ! y. q(x) = q(y))  =		\
 \                   ((? x. p(x)) = (! y. q(y))))";
-by (safe_tac HOL_cs);			(*24 secs*)
-by (TRYALL (fast_tac HOL_cs));		(*161 secs*)
-by (TRYALL (best_tac HOL_dup_cs));	(*86 secs -- much faster than FOL!*)
+by (deepen_tac HOL_cs 3 1);
+(*slower with smaller bounds*)
 result();
 
 writeln"Problem 35";
 goal HOL.thy "? x y. P(x,y) -->  (! u v. P(u,v))";
-by (best_tac HOL_dup_cs 1);
+by (deepen_tac HOL_cs 1 1);
 result();
 
 writeln"Problem 36";
@@ -337,6 +336,8 @@
 
 writeln"Problem 42";
 goal HOL.thy "~ (? y. ! x. p(x,y) = (~ (? z. p(x,z) & p(z,x))))";
+by (deepen_tac HOL_cs 3 1);
+result();
 
 writeln"Problem 43  NOT PROVED AUTOMATICALLY";
 goal HOL.thy
@@ -387,7 +388,7 @@
 writeln"Problem 50";  
 (*What has this to do with equality?*)
 goal HOL.thy "(! x. P(a,x) | (! y.P(x,y))) --> (? x. ! y.P(x,y))";
-by (best_tac HOL_dup_cs 1);
+by (deepen_tac HOL_cs 1 1);
 result();
 
 writeln"Problem 51";
@@ -442,7 +443,7 @@
 
 writeln"Problem 59";
 goal HOL.thy "(! x. P(x) = (~P(f(x)))) --> (? x. P(x) & ~P(f(x)))";
-by (best_tac HOL_dup_cs 1);
+by (deepen_tac HOL_cs 1 1);
 result();
 
 writeln"Problem 60";