[isabelle-dev] case syntax
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.
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