On 03/23/2012 11:45 AM, Jesus Aransay wrote:
I know there is an alternative way to get that, by means of sparse
matrices (SparseMatrix.thy), but it demands translating every
operation over the matrix type to its equivalent version for sparse
matrices, which may be sometimes hard work.
Code
On Fri, 23 Mar 2012, Christian Sternagel wrote:
Maybe the AFP entry for executable matrix operations is useful for you.
http://afp.sourceforge.net/entries/Matrix.shtml
(HOL/Matrix/Matrix.thy).
Note that in current Isabelle/08c22e8ffe70 HOL/Matrix is actually called
HOL/Matrix_LP, in order
Absolutely, thanks. Constants should be hidden if they are internal to some
package. Especially with such a universal name as invariant.
Tobias
Am 23/03/2012 17:34, schrieb Makarius:
Just a note on the following changeset:
changeset: 47095:3ea48c19673e
user:kuncar
date:
On 03/23/2012 05:34 PM, Makarius wrote:
Just a note on the following changeset:
changeset: 47095:3ea48c19673e
user: kuncar
date: Fri Mar 23 14:25:31 2012 +0100
files: src/HOL/Quotient.thy src/HOL/Tools/Quotient/quotient_def.ML
src/HOL/Tools/Quotient/quotient_term.ML
If it turns out that the constant is not internal-only, it should get a more
specific name. invariant really is a name that should be available to users
without shadowing.
Cheers,
Gerwin
On 24/03/2012, at 4:06, Ondřej Kunčar kun...@in.tum.de wrote:
On 03/23/2012 05:34 PM, Makarius wrote:
