# HG changeset patch
# User wenzelm
# Date 1001622200 -7200
# Node ID c3724decadefdd0780d61d8b98a83e8682ff1d80
# Parent  bf6700f4c0102c949c57e816d8b2517bb663c3fb
tuned:

diff -r bf6700f4c010 -r c3724decadef src/HOL/equalities.ML
--- a/src/HOL/equalities.ML	Thu Sep 27 22:22:58 2001 +0200
+++ b/src/HOL/equalities.ML	Thu Sep 27 22:23:20 2001 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/equalities
+(*  Title:      HOL/equalities.ML
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1994  University of Cambridge
@@ -6,8 +6,6 @@
 Equalities involving union, intersection, inclusion, etc.
 *)
 
-writeln"File HOL/equalities";
-
 AddSIs [equalityI];
 
 section "{}";
diff -r bf6700f4c010 -r c3724decadef src/HOL/subset.ML
--- a/src/HOL/subset.ML	Thu Sep 27 22:22:58 2001 +0200
+++ b/src/HOL/subset.ML	Thu Sep 27 22:23:20 2001 +0200
@@ -1,10 +1,10 @@
-(*  Title:      HOL/subset
+(*  Title:      HOL/subset.ML
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
 
-Derived rules involving subsets
-Union and Intersection as lattice operations
+Derived rules involving subsets.  Union and Intersection as lattice
+operations.
 *)
 
 (*** insert ***)