src/HOL/simpdata.ML
changeset 4794 9db0916ecdae
parent 4769 bb60149fe21b
child 4830 bd73675adbed
     1.1 --- a/src/HOL/simpdata.ML	Sat Apr 04 12:28:39 1998 +0200
     1.2 +++ b/src/HOL/simpdata.ML	Sat Apr 04 12:29:07 1998 +0200
     1.3 @@ -3,13 +3,11 @@
     1.4      Author:     Tobias Nipkow
     1.5      Copyright   1991  University of Cambridge
     1.6  
     1.7 -Instantiation of the generic simplifier
     1.8 +Instantiation of the generic simplifier.
     1.9  *)
    1.10  
    1.11  section "Simplifier";
    1.12  
    1.13 -open Simplifier;
    1.14 -
    1.15  (*** Addition of rules to simpsets and clasets simultaneously ***)
    1.16  
    1.17  (*Takes UNCONDITIONAL theorems of the form A<->B to 
    1.18 @@ -450,9 +448,6 @@
    1.19  
    1.20  
    1.21  
    1.22 -
    1.23 -
    1.24 -
    1.25  (*** Integration of simplifier with classical reasoner ***)
    1.26  
    1.27  (* rot_eq_tac rotates the first equality premise of subgoal i to the front,