no open Simplifier;
authorwenzelm
Sat Apr 04 12:29:07 1998 +0200 (1998-04-04)
changeset 47949db0916ecdae
parent 4793 03fd006fb97b
child 4795 721b532ada7a
no open Simplifier;
src/FOL/simpdata.ML
src/HOL/simpdata.ML
     1.1 --- a/src/FOL/simpdata.ML	Sat Apr 04 12:28:39 1998 +0200
     1.2 +++ b/src/FOL/simpdata.ML	Sat Apr 04 12:29:07 1998 +0200
     1.3 @@ -188,8 +188,6 @@
     1.4    (fn [prem] => [rewtac prem, rtac refl 1]);
     1.5  
     1.6  
     1.7 -open Simplifier;
     1.8 -
     1.9  (** make simplification procedures for quantifier elimination **)
    1.10  structure Quantifier1 = Quantifier1Fun(
    1.11  struct
     2.1 --- a/src/HOL/simpdata.ML	Sat Apr 04 12:28:39 1998 +0200
     2.2 +++ b/src/HOL/simpdata.ML	Sat Apr 04 12:29:07 1998 +0200
     2.3 @@ -3,13 +3,11 @@
     2.4      Author:     Tobias Nipkow
     2.5      Copyright   1991  University of Cambridge
     2.6  
     2.7 -Instantiation of the generic simplifier
     2.8 +Instantiation of the generic simplifier.
     2.9  *)
    2.10  
    2.11  section "Simplifier";
    2.12  
    2.13 -open Simplifier;
    2.14 -
    2.15  (*** Addition of rules to simpsets and clasets simultaneously ***)
    2.16  
    2.17  (*Takes UNCONDITIONAL theorems of the form A<->B to 
    2.18 @@ -450,9 +448,6 @@
    2.19  
    2.20  
    2.21  
    2.22 -
    2.23 -
    2.24 -
    2.25  (*** Integration of simplifier with classical reasoner ***)
    2.26  
    2.27  (* rot_eq_tac rotates the first equality premise of subgoal i to the front,