Hi Walther,
in addition to the hints given by Christian, I add that it appears to me
that you just want to do equational rewriting on bare terms. For this
you can use Pattern.rewrite_term
Hope this helps,
Florian
--
Home:
http://www.in.tum.de/~haftmann
PGP available:
Hi Christian,
thanks for the code !
The code was helpful to set my wits to combinators. And it gave another
good exercise to distinguish what should be related to contexts and what
to theories (formulas of concrete calculations to the former, and
predefined patterns like those describing
On 10/01/2010 08:49 AM, Florian Haftmann wrote:
Hi Walther,
in addition to the hints given by Christian, I add that it appears to me
that you just want to do equational rewriting on bare terms. For this
you can use Pattern.rewrite_term
Florian, thanks for this hint !
We are highly aware
Hi all,
Last week I experienced strange errors on my machine regarding mkdir on my
Mac (with Nitpick and Sledgehammer), but these eventually went away after I
pulled a newer version of Isabelle.
Now I'm testing on macbroy2 and getting similar errors, but this time in
Imperative HOL:
***
On Fri, 1 Oct 2010, Jasmin Blanchette wrote:
Last week I experienced strange errors on my machine regarding mkdir
on my Mac (with Nitpick and Sledgehammer), but these eventually went
away after I pulled a newer version of Isabelle.
Now I'm testing on macbroy2 and getting similar errors, but
Am 01.10.2010 um 17:03 schrieb Makarius:
On Fri, 1 Oct 2010, Jasmin Blanchette wrote:
[...]
Has anybody run into similar issues before?
Yes, it merely means there is an inconsistency between the sources (notably
lib/scripts/process) and the compiled image. You merely need to make sure
