On Sun, 13 May 2012, Florian Haftmann wrote:
c) I strongly object to clutter the HOL syntax even more than now by
incorporating just another fancy syntax. I would prefer the lattice
solution (delete syntax immediately after use and provide a library
theory to optionally include it later), or
Hi Makarius,
At some point, when I have bundles ready to work with the existing
notation commands, we can fine-tune this scheme further, to allow users to
'include' syntax in local situations.
I tried to implement the new syntax for FinFuns with bundles and Brian's
notation attribute
On Thu, May 31, 2012 at 1:36 PM, Makarius makar...@sketis.net wrote:
On Thu, 31 May 2012, Andreas Lochbihler wrote:
At some point, when I have bundles ready to work with the existing
notation commands, we can fine-tune this scheme further, to allow users
to
'include' syntax in local
On Thu, 31 May 2012, Brian Huffman wrote:
On Thu, May 31, 2012 at 1:36 PM, Makarius makar...@sketis.net wrote:
On Thu, 31 May 2012, Andreas Lochbihler wrote:
At some point, when I have bundles ready to work with the existing
notation commands, we can fine-tune this scheme further, to allow
Hi all,
In the short term, we could move the FinFun theory into the HOL library
of the development version after Isabelle 2012 and the AFP 2012 has been
released, if we agree that this moves this contribution in the right
direction.
some remarks on my behalf:
a) Ideally, tools
Dear All,
In Nominal I am usually relying on types that are defined
in HOL or that I define myself. However, I now came across
the FinFun development in the AFP by Andreas Lochbihler (thanks
to Larry). The finfun type seems to be rather useful to Nominal
users, since it has finite support, in
Hi Christian,
For code generation purposes and especially Quickcheck, it is necessary
that the FinFun theory would be imported by any user.
With the new developments lifting and transfer, we are getting very
close that FinFun can be used without any further ado.
I do have some latest
