removal of FOL_dup_cs
Fri, 11 Nov 1994 10:53:41 +0100
changeset 706 31b1e4f9af30
parent 705 9fb068497df4
child 707 04d661f1d2f8
removal of FOL_dup_cs
--- a/doc-src/Logics/FOL.tex	Fri Nov 11 10:50:49 1994 +0100
+++ b/doc-src/Logics/FOL.tex	Fri Nov 11 10:53:41 1994 +0100
@@ -339,7 +339,6 @@
 prop_cs    : claset
 FOL_cs     : claset
-FOL_dup_cs : claset
 \item[\ttindexbold{prop_cs}] contains the propositional rules, namely
@@ -351,13 +350,6 @@
 and the unsafe rules {\tt allE} and~{\tt exI}, as well as rules for
 unique existence.  Search using this is incomplete since quantified
 formulae are used at most once.
-extends {\tt prop_cs} with the safe rules {\tt allI} and~{\tt exE}
-and the unsafe rules {\tt all_dupE} and~{\tt exCI}, as well as
-rules for unique existence.  Search using this is complete --- quantified
-formulae may be duplicated --- but frequently fails to terminate.  It is
-generally unsuitable for depth-first search.
 See the file {\tt FOL/FOL.ML} for derivations of the