# HG changeset patch
# User wenzelm
# Date 1119298441 -7200
# Node ID 2060ebae96f945ba35bb01ffc4f84d64b62f879a
# Parent  1a12cdb6ee6b7352c256c1ae4b53ff7fe8b8c025
proper header;

diff -r 1a12cdb6ee6b -r 2060ebae96f9 src/HOL/Matrix/ROOT.ML
--- 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";
+
diff -r 1a12cdb6ee6b -r 2060ebae96f9 src/HOL/Matrix/SparseMatrix.thy
--- 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