Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Matrix/cplex/FloatSparseMatrix.thy
author huffman
Thu, 03 Jul 2008 20:53:44 +0200
changeset 27483 7c58324cd418
parent 27298 a5373b60e66c
permissions -rw-r--r--
use real_of_nat_ge_zero instead of real_of_nat_fact_ge_zero
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset 
     1
 
(*  Title:      HOL/Matrix/cplex/FloatSparseMatrix.thy
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset 
     2
 
    ID:         $Id$
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset 
     3
 
    Author:     Steven Obua
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset 
     4
 
*)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset 
     5
 







27298






a5373b60e66c
moved Float.thy to Library



haftmann


parents: 
16890

diff
changeset




     6


theory FloatSparseMatrix













a5373b60e66c
moved Float.thy to Library



haftmann


parents: 
16890

diff
changeset




     7


imports "../../Real/Float" SparseMatrix













a5373b60e66c
moved Float.thy to Library



haftmann


parents: 
16890

diff
changeset




     8


begin








16784






92ff7c903585
- added cplex package to HOL/Matrix



obua


parents: 

diff
changeset




     9














92ff7c903585
- added cplex package to HOL/Matrix



obua


parents: 

diff
changeset




    10


end















isabelle