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