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