[isabelle-dev] case syntax

[Stefan Berghofer]

Quoting Makarius <makarius at sketis.net>:
> Just to illuminate the general situation a bit, can you point to  
> relevant parts of your thesis, also the one of Konrad Slind for the  
> old version? Stefan had mentioned that at some point "as everybody  
> knows, Konrad used to do it like that" without giving a reference.

Hi Markus,

you can find Konrad's thesis on the web at

   http://www.cl.cam.ac.uk/~ks121/papers/phd.html

The pattern matching algorithm is described in Section 3.3 (p. 62 - 71)
The steps of the algorithm are summarized in Figure 3.4.

Greetings,
Stefan