I used a literal ~ and changing this to $HOME solved the problem,
thanks!
cheers
chris
PS: Is it just me or is Isabelle/jEdit really much faster than
ProofGeneral/emacs when loading theories? (Maybe this is due to some
other difference between Isabelle2011-1 and the repo version; I only use
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
On Wed, 21 Mar 2012, Christian Sternagel wrote:
Is it just me or is Isabelle/jEdit really much faster than
ProofGeneral/emacs when loading theories? (Maybe this is due to some
other difference between Isabelle2011-1 and the repo version; I only use
emacs if I have to stick to Isabelle2011-1.)
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
