# HG changeset patch # User lcp # Date 790912921 -3600 # Node ID 2432820efbfeaa9e200ba019718b6fd57c27a617 # Parent 0cfc734e3dbda52b07c75c7fc87033e298329227 removed mention of FOL_dup_cs diff -r 0cfc734e3dbd -r 2432820efbfe doc-src/Logics/FOL.tex --- a/doc-src/Logics/FOL.tex Tue Jan 24 03:01:14 1995 +0100 +++ b/doc-src/Logics/FOL.tex Tue Jan 24 03:02:01 1995 +0100 @@ -614,14 +614,16 @@ {\out EX y. ALL x. P(y) --> P(x)} {\out No subgoals!} \end{ttbox} -The civilised way to prove this theorem is through \ttindex{best_tac}, -supplying the classical version of~$(\exists I)$: +The civilised way to prove this theorem is through \ttindex{deepen_tac}, +which automatically uses the classical version of~$(\exists I)$: \begin{ttbox} goal FOL.thy "EX y. ALL x. P(y)-->P(x)"; {\out Level 0} {\out EX y. ALL x. P(y) --> P(x)} {\out 1. EX y. ALL x. P(y) --> P(x)} -by (best_tac FOL_dup_cs 1); +by (deepen_tac FOL_cs 0 1); +{\out Depth = 0} +{\out Depth = 2} {\out Level 1} {\out EX y. ALL x. P(y) --> P(x)} {\out No subgoals!}