equal
deleted
inserted
replaced
5 *) |
5 *) |
6 |
6 |
7 header {* Weak normalization for simply-typed lambda calculus *} |
7 header {* Weak normalization for simply-typed lambda calculus *} |
8 |
8 |
9 theory WeakNorm |
9 theory WeakNorm |
10 imports Type NormalForm Pretty_Int |
10 imports Type NormalForm Code_Integer |
11 begin |
11 begin |
12 |
12 |
13 text {* |
13 text {* |
14 Formalization by Stefan Berghofer. Partly based on a paper proof by |
14 Formalization by Stefan Berghofer. Partly based on a paper proof by |
15 Felix Joachimski and Ralph Matthes \cite{Matthes-Joachimski-AML}. |
15 Felix Joachimski and Ralph Matthes \cite{Matthes-Joachimski-AML}. |