added HOL-Matrix, added HOL/Matrix/ROOT.ML
authorkleing
Sat Apr 17 00:46:22 2004 +0200 (2004-04-17)
changeset 146109c2e31e483b2
parent 14609 663e0e435866
child 14611 e9d2f771b3c7
added HOL-Matrix, added HOL/Matrix/ROOT.ML
NEWS
src/HOL/IsaMakefile
src/HOL/Matrix/ROOT.ML
     1.1 --- a/NEWS	Fri Apr 16 21:03:40 2004 +0200
     1.2 +++ b/NEWS	Sat Apr 17 00:46:22 2004 +0200
     1.3 @@ -143,7 +143,10 @@
     1.4  * HOL-Algebra: new locale "ring" for non-commutative rings.
     1.5  
     1.6  * HOL-ex: InductiveInvariant_examples illustrates advanced recursive function
     1.7 - defintions, thanks to Sava Krsti\'{c} and John Matthews.
     1.8 +  definitions, thanks to Sava Krsti\'{c} and John Matthews.
     1.9 +
    1.10 +* HOL-Matrix: a first theory for matrices in HOL with an application of 
    1.11 +  matrix theory to linear programming.
    1.12  
    1.13  * Unions and Intersections:
    1.14    The x-symbol output syntax of UN and INT has been changed
     2.1 --- a/src/HOL/IsaMakefile	Fri Apr 16 21:03:40 2004 +0200
     2.2 +++ b/src/HOL/IsaMakefile	Sat Apr 17 00:46:22 2004 +0200
     2.3 @@ -29,6 +29,7 @@
     2.4    HOL-Isar_examples \
     2.5    HOL-Lambda \
     2.6    HOL-Lattice \
     2.7 +  HOL-Matrix \
     2.8    HOL-MicroJava \
     2.9    HOL-Modelcheck \
    2.10    HOL-NanoJava \
    2.11 @@ -632,6 +633,17 @@
    2.12  	@$(ISATOOL) usedir -g true $(OUT)/HOL SET-Protocol
    2.13  
    2.14  
    2.15 +## HOL-Matrix
    2.16 +
    2.17 +HOL-Matrix: HOL $(LOG)/HOL-Matrix.gz
    2.18 +
    2.19 +$(LOG)/HOL-Matrix.gz: $(OUT)/HOL Matrix/ROOT.ML \
    2.20 +  Matrix/Matrix.thy\
    2.21 +	Matrix/LinProg.thy\
    2.22 +	Matrix/MatrixGeneral.thy
    2.23 +	@$(ISATOOL) usedir $(OUT)/HOL Matrix
    2.24 +
    2.25 +
    2.26  
    2.27  ## TLA
    2.28  
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Matrix/ROOT.ML	Sat Apr 17 00:46:22 2004 +0200
     3.3 @@ -0,0 +1,1 @@
     3.4 +use_thy "LinProg";