equal
deleted
inserted
replaced
7 |
7 |
8 theory StrongNorm imports LambdaType 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 *} |
14 |
14 |
15 |
15 |
16 subsection {* Properties of @{text IT} *} |
16 subsection {* Properties of @{text IT} *} |
17 |
17 |