equal
deleted
inserted
replaced
3 Copyright 2000 TU Muenchen |
3 Copyright 2000 TU Muenchen |
4 *) |
4 *) |
5 |
5 |
6 header {* Strong normalization for simply-typed lambda calculus *} |
6 header {* Strong normalization for simply-typed lambda calculus *} |
7 |
7 |
8 theory StrongNorm imports Type InductTermi begin |
8 theory StrongNorm imports LambdaType InductTermi begin |
9 |
9 |
10 text {* |
10 text {* |
11 Formalization by Stefan Berghofer. Partly based on a paper proof by |
11 Formalization by Stefan Berghofer. Partly based on a paper proof by |
12 Felix Joachimski and Ralph Matthes \cite{Matthes-Joachimski-AML}. |
12 Felix Joachimski and Ralph Matthes \cite{Matthes-Joachimski-AML}. |
13 *} |
13 *} |