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