--- 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
--- 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"