On Tue, 27 Mar 2012, Jesus Aransay wrote:
trying to import simultaneously the theory file
HOL/Matrix/Matrix.thy and the afp entry
http://afp.sourceforge.net/entries/Matrix.shtml into a file
theory Matrix_ex
imports
~~/src/HOL/Matrix/Matrix
Matrix/Matrix
begin
Is there an easy way out of
Hi Jesus,
trying to import simultaneously the theory file
HOL/Matrix/Matrix.thy and the afp entry
http://afp.sourceforge.net/entries/Matrix.shtml into a file, it seems
that the second theory file unloads the first one (as Makarius
suggested in his mail):
theory Matrix_ex
imports
Dear all,
trying to import simultaneously the theory file
HOL/Matrix/Matrix.thy and the afp entry
http://afp.sourceforge.net/entries/Matrix.shtml into a file, it seems
that the second theory file unloads the first one (as Makarius
suggested in his mail):
theory Matrix_ex
imports
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
Hi there,
since set is a proper type some code equations that used to work, no
longer do, e.g.,
op | = {(x, y). supt_impl x y}
as a code equation leads to an error stating that terms (x and y are
first-order terms) do not support the enum class. Since the possible
terms (using strings as
On 03/21/2012 08:36 AM, Christian Sternagel wrote:
Hi there,
since set is a proper type some code equations that used to work, no
longer do, e.g.,
op | = {(x, y). supt_impl x y}
as a code equation leads to an error stating that terms (x and y are
first-order terms) do not support the enum
On 03/21/2012 05:05 PM, Lukas Bulwahn wrote:
On 03/21/2012 08:36 AM, Christian Sternagel wrote:
Hi there,
since set is a proper type some code equations that used to work, no
longer do, e.g.,
op | = {(x, y). supt_impl x y}
as a code equation leads to an error stating that terms (x and y are
On 03/21/2012 09:08 AM, Christian Sternagel wrote:
On 03/21/2012 05:05 PM, Lukas Bulwahn wrote:
On 03/21/2012 08:36 AM, Christian Sternagel wrote:
Hi there,
since set is a proper type some code equations that used to work, no
longer do, e.g.,
op | = {(x, y). supt_impl x y}
as a code
Hi Christian,
since set is a proper type some code equations that used to work, no
longer do, e.g.,
op | = {(x, y). supt_impl x y}
there is a couple of issues you are hitting at here.
A. The (re-)introduction of the set type constructor
See
10 matches
Mail list logo
