[isabelle-dev] case syntax

Stefan Berghofer berghofe at in.tum.de
Thu Jan 12 15:43:05 CET 2012

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


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


More information about the isabelle-dev mailing list