| changeset 4794 | 9db0916ecdae |
| parent 4669 | 06f3c56dcba8 |
| child 4930 | 89271bc4e7ed |
--- a/src/FOL/simpdata.ML Sat Apr 04 12:28:39 1998 +0200 +++ b/src/FOL/simpdata.ML Sat Apr 04 12:29:07 1998 +0200 @@ -188,8 +188,6 @@ (fn [prem] => [rewtac prem, rtac refl 1]); -open Simplifier; - (** make simplification procedures for quantifier elimination **) structure Quantifier1 = Quantifier1Fun( struct