# HG changeset patch
# User kleing
# Date 1082155582 -7200
# Node ID 9c2e31e483b277c10b86247faeb84655535a644a
# Parent  663e0e435866c0df5ff4f27d8407d070c3097bb6
added HOL-Matrix, added HOL/Matrix/ROOT.ML

diff -r 663e0e435866 -r 9c2e31e483b2 NEWS
--- a/NEWS	Fri Apr 16 21:03:40 2004 +0200
+++ b/NEWS	Sat Apr 17 00:46:22 2004 +0200
@@ -143,7 +143,10 @@
 * HOL-Algebra: new locale "ring" for non-commutative rings.
 
 * HOL-ex: InductiveInvariant_examples illustrates advanced recursive function
- defintions, thanks to Sava Krsti\'{c} and John Matthews.
+  definitions, thanks to Sava Krsti\'{c} and John Matthews.
+
+* HOL-Matrix: a first theory for matrices in HOL with an application of 
+  matrix theory to linear programming.
 
 * Unions and Intersections:
   The x-symbol output syntax of UN and INT has been changed
diff -r 663e0e435866 -r 9c2e31e483b2 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Apr 16 21:03:40 2004 +0200
+++ b/src/HOL/IsaMakefile	Sat Apr 17 00:46:22 2004 +0200
@@ -29,6 +29,7 @@
   HOL-Isar_examples \
   HOL-Lambda \
   HOL-Lattice \
+  HOL-Matrix \
   HOL-MicroJava \
   HOL-Modelcheck \
   HOL-NanoJava \
@@ -632,6 +633,17 @@
 	@$(ISATOOL) usedir -g true $(OUT)/HOL SET-Protocol
 
 
+## HOL-Matrix
+
+HOL-Matrix: HOL $(LOG)/HOL-Matrix.gz
+
+$(LOG)/HOL-Matrix.gz: $(OUT)/HOL Matrix/ROOT.ML \
+  Matrix/Matrix.thy\
+	Matrix/LinProg.thy\
+	Matrix/MatrixGeneral.thy
+	@$(ISATOOL) usedir $(OUT)/HOL Matrix
+
+
 
 ## TLA
 
diff -r 663e0e435866 -r 9c2e31e483b2 src/HOL/Matrix/ROOT.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Matrix/ROOT.ML	Sat Apr 17 00:46:22 2004 +0200
@@ -0,0 +1,1 @@
+use_thy "LinProg";