isatool fixheaders;
authorwenzelm
Wed Oct 19 21:52:27 2005 +0200 (2005-10-19)
changeset 17915e38947f9ba5e
parent 17914 99ead7a7eb42
child 17916 51269a053504
isatool fixheaders;
src/HOL/Import/HOLLight/HOLLight.thy
src/HOL/Matrix/Matrix.thy
     1.1 --- a/src/HOL/Import/HOLLight/HOLLight.thy	Wed Oct 19 21:52:07 2005 +0200
     1.2 +++ b/src/HOL/Import/HOLLight/HOLLight.thy	Wed Oct 19 21:52:27 2005 +0200
     1.3 @@ -1,6 +1,6 @@
     1.4  (* AUTOMATICALLY GENERATED, DO NOT EDIT! *)
     1.5  
     1.6 -theory HOLLight = "../HOLLightCompat" + "../HOL4Syntax":
     1.7 +theory HOLLight imports "../HOLLightCompat" "../HOL4Syntax" begin
     1.8  
     1.9  ;setup_theory hollight
    1.10  
     2.1 --- a/src/HOL/Matrix/Matrix.thy	Wed Oct 19 21:52:07 2005 +0200
     2.2 +++ b/src/HOL/Matrix/Matrix.thy	Wed Oct 19 21:52:27 2005 +0200
     2.3 @@ -3,16 +3,15 @@
     2.4      Author:     Steven Obua
     2.5  *)
     2.6  
     2.7 -theory Matrix=MatrixGeneral:
     2.8 -
     2.9 -instance matrix :: (minus) minus 
    2.10 -by intro_classes
    2.11 +theory Matrix
    2.12 +imports MatrixGeneral
    2.13 +begin
    2.14  
    2.15 -instance matrix :: (plus) plus
    2.16 -by (intro_classes)
    2.17 +instance matrix :: (minus) minus ..
    2.18  
    2.19 -instance matrix :: ("{plus,times}") times
    2.20 -by (intro_classes)
    2.21 +instance matrix :: (plus) plus ..
    2.22 +
    2.23 +instance matrix :: ("{plus,times}") times ..
    2.24  
    2.25  defs (overloaded)
    2.26    plus_matrix_def: "A + B == combine_matrix (op +) A B"