[isabelle-dev] use term patterns, was: 'produce term patterns'
wneuper at ist.tugraz.at
Fri Oct 1 09:27:22 CEST 2010
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,
More information about the isabelle-dev