--- 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
--- a/src/HOL/simpdata.ML Sat Apr 04 12:28:39 1998 +0200
+++ b/src/HOL/simpdata.ML Sat Apr 04 12:29:07 1998 +0200
@@ -3,13 +3,11 @@
Author: Tobias Nipkow
Copyright 1991 University of Cambridge
-Instantiation of the generic simplifier
+Instantiation of the generic simplifier.
*)
section "Simplifier";
-open Simplifier;
-
(*** Addition of rules to simpsets and clasets simultaneously ***)
(*Takes UNCONDITIONAL theorems of the form A<->B to
@@ -450,9 +448,6 @@
-
-
-
(*** Integration of simplifier with classical reasoner ***)
(* rot_eq_tac rotates the first equality premise of subgoal i to the front,