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 of the advantages of Isabelle's rewriting machinery;
for re-animating our code we have to rely on our own rewriter (which
handles predicates like "(a + b * x) is_polynomial & 0 is_polynomial",
while "is_polynomial" calls ML code) --- but then we shall learn to use
Isabelle's "logical operating system";
Hope this helps,
Florian
Walther
_______________________________________________
Isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
