proper header;
authorwenzelm
Mon Jun 20 22:14:01 2005 +0200 (2005-06-20)
changeset 164872060ebae96f9
parent 16486 1a12cdb6ee6b
child 16488 38bc902946b2
proper header;
src/HOL/Matrix/ROOT.ML
src/HOL/Matrix/SparseMatrix.thy
     1.1 --- a/src/HOL/Matrix/ROOT.ML	Mon Jun 20 22:13:59 2005 +0200
     1.2 +++ b/src/HOL/Matrix/ROOT.ML	Mon Jun 20 22:14:01 2005 +0200
     1.3 @@ -1,1 +1,6 @@
     1.4 -use_thy "SparseMatrix"
     1.5 +(*  Title:      HOL/Matrix/ROOT.ML
     1.6 +    ID:         $Id$
     1.7 +*)
     1.8 +
     1.9 +use_thy "SparseMatrix";
    1.10 +
     2.1 --- a/src/HOL/Matrix/SparseMatrix.thy	Mon Jun 20 22:13:59 2005 +0200
     2.2 +++ b/src/HOL/Matrix/SparseMatrix.thy	Mon Jun 20 22:14:01 2005 +0200
     2.3 @@ -1,3 +1,8 @@
     2.4 +(*  Title:      HOL/Matrix/SparseMatrix.thy
     2.5 +    ID:         $Id$
     2.6 +    Author:     Steven Obua
     2.7 +*)
     2.8 +
     2.9  theory SparseMatrix imports Matrix begin
    2.10  
    2.11  types