[isabelle-dev] use term patterns, was: 'produce term patterns'

[Walther Neuper]

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