--- a/src/HOL/Matrix/ROOT.ML Mon Jun 20 22:13:59 2005 +0200
+++ b/src/HOL/Matrix/ROOT.ML Mon Jun 20 22:14:01 2005 +0200
@@ -1,1 +1,6 @@
-use_thy "SparseMatrix"
+(* Title: HOL/Matrix/ROOT.ML
+ ID: $Id$
+*)
+
+use_thy "SparseMatrix";
+
--- a/src/HOL/Matrix/SparseMatrix.thy Mon Jun 20 22:13:59 2005 +0200
+++ b/src/HOL/Matrix/SparseMatrix.thy Mon Jun 20 22:14:01 2005 +0200
@@ -1,3 +1,8 @@
+(* Title: HOL/Matrix/SparseMatrix.thy
+ ID: $Id$
+ Author: Steven Obua
+*)
+
theory SparseMatrix imports Matrix begin
types