[isabelle-dev] Pattern.match -- a minute

[Walther Neuper]

Dear Christian,

Thank you for pointing me at the Programming Tutorial -- I see it
greatly improved since the Isabelle Workshop last summer.

Now the latest version is in my local library and will help a lot,
indeed, thank you !

Walther

Christian Urban wrote:
> Dear Walther,
> 
> About your second question: there is a section 
> about using the function Pattern.match in the 
> Programming Tutorial ([1], Section 3.3). 
> It should  
> explain how to do such pattern match examples.
> The main contortion below probably comes from the 
> parsing of input. Since the antiquotation @{term ...} 
> does not allow schematic variables, I written a small
> antiquotation @{term_pat ...} that is explained 
> section 2.4 and which allows such input terms to
> be given directly. All should be conveniently 
> referenced.
> 
> Hope this helps,
> Christian