# HG changeset patch
# User wenzelm
# Date 1129751547 -7200
# Node ID e38947f9ba5ed9008fc015119cd21911bfcf00a7
# Parent  99ead7a7eb42bf044fe6e22f5bbe4f778512d4f9
isatool fixheaders;

diff -r 99ead7a7eb42 -r e38947f9ba5e src/HOL/Import/HOLLight/HOLLight.thy
--- a/src/HOL/Import/HOLLight/HOLLight.thy	Wed Oct 19 21:52:07 2005 +0200
+++ b/src/HOL/Import/HOLLight/HOLLight.thy	Wed Oct 19 21:52:27 2005 +0200
@@ -1,6 +1,6 @@
 (* AUTOMATICALLY GENERATED, DO NOT EDIT! *)
 
-theory HOLLight = "../HOLLightCompat" + "../HOL4Syntax":
+theory HOLLight imports "../HOLLightCompat" "../HOL4Syntax" begin
 
 ;setup_theory hollight
 
diff -r 99ead7a7eb42 -r e38947f9ba5e src/HOL/Matrix/Matrix.thy
--- a/src/HOL/Matrix/Matrix.thy	Wed Oct 19 21:52:07 2005 +0200
+++ b/src/HOL/Matrix/Matrix.thy	Wed Oct 19 21:52:27 2005 +0200
@@ -3,16 +3,15 @@
     Author:     Steven Obua
 *)
 
-theory Matrix=MatrixGeneral:
-
-instance matrix :: (minus) minus 
-by intro_classes
+theory Matrix
+imports MatrixGeneral
+begin
 
-instance matrix :: (plus) plus
-by (intro_classes)
+instance matrix :: (minus) minus ..
 
-instance matrix :: ("{plus,times}") times
-by (intro_classes)
+instance matrix :: (plus) plus ..
+
+instance matrix :: ("{plus,times}") times ..
 
 defs (overloaded)
   plus_matrix_def: "A + B == combine_matrix (op +) A B"