Removal of obsolete "open" commands from heads of .ML files
authorpaulson
Fri Jul 31 11:03:21 1998 +0200 (1998-07-31)
changeset 5227e5a6ace920a0
parent 5226 89934cd022a9
child 5228 66925577cefe
Removal of obsolete "open" commands from heads of .ML files
src/HOL/ex/BT.ML
src/HOL/ex/IntRing.ML
src/HOL/ex/IntRingDefs.ML
src/HOL/ex/MT.ML
src/HOL/ex/Primes.ML
     1.1 --- a/src/HOL/ex/BT.ML	Fri Jul 31 10:54:39 1998 +0200
     1.2 +++ b/src/HOL/ex/BT.ML	Fri Jul 31 11:03:21 1998 +0200
     1.3 @@ -6,8 +6,6 @@
     1.4  Datatype definition of binary trees
     1.5  *)
     1.6  
     1.7 -open BT;
     1.8 -
     1.9  (** BT simplification **)
    1.10  
    1.11  Goal "n_leaves(reflect(t)) = n_leaves(t)";
     2.1 --- a/src/HOL/ex/IntRing.ML	Fri Jul 31 10:54:39 1998 +0200
     2.2 +++ b/src/HOL/ex/IntRing.ML	Fri Jul 31 11:03:21 1998 +0200
     2.3 @@ -6,8 +6,6 @@
     2.4  The instantiation of Lagrange's lemma for int.
     2.5  *)
     2.6  
     2.7 -open IntRing;
     2.8 -
     2.9  Goal "!!i1::int. \
    2.10  \  (sq i1 + sq i2 + sq i3 + sq i4) * (sq j1 + sq j2 + sq j3 + sq j4) = \
    2.11  \  sq(i1*j1 - i2*j2 - i3*j3 - i4*j4)  + \
     3.1 --- a/src/HOL/ex/IntRingDefs.ML	Fri Jul 31 10:54:39 1998 +0200
     3.2 +++ b/src/HOL/ex/IntRingDefs.ML	Fri Jul 31 11:03:21 1998 +0200
     3.3 @@ -2,11 +2,8 @@
     3.4      ID:         $Id$
     3.5      Author:     Tobias Nipkow and Markus Wenzel
     3.6      Copyright   1996 TU Muenchen
     3.7 -
     3.8  *)
     3.9  
    3.10 -open IntRingDefs;
    3.11 -
    3.12  Goalw [zero_int_def,zdiff_def] "(zero-x)+(x::int) = zero";
    3.13  by (Simp_tac 1);
    3.14  qed "left_inv_int";
     4.1 --- a/src/HOL/ex/MT.ML	Fri Jul 31 10:54:39 1998 +0200
     4.2 +++ b/src/HOL/ex/MT.ML	Fri Jul 31 11:03:21 1998 +0200
     4.3 @@ -15,8 +15,6 @@
     4.4  NEEDS TO USE INDUCTIVE DEFS PACKAGE
     4.5  *)
     4.6  
     4.7 -open MT;
     4.8 -
     4.9  (* ############################################################ *)
    4.10  (* Inference systems                                            *)
    4.11  (* ############################################################ *)
     5.1 --- a/src/HOL/ex/Primes.ML	Fri Jul 31 10:54:39 1998 +0200
     5.2 +++ b/src/HOL/ex/Primes.ML	Fri Jul 31 11:03:21 1998 +0200
     5.3 @@ -10,8 +10,6 @@
     5.4  
     5.5  eta_contract:=false;
     5.6  
     5.7 -open Primes;
     5.8 -
     5.9  (************************************************)
    5.10  (** Greatest Common Divisor                    **)
    5.11  (************************************************)