--- 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 "{}";
--- 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 ***)