equal
deleted
inserted
replaced
1 (* Title: HOL/Proofs/Lambda/StrongNorm.thy |
1 (* Title: HOL/Proofs/Lambda/StrongNorm.thy |
2 Author: Stefan Berghofer |
2 Author: Stefan Berghofer |
3 Copyright 2000 TU Muenchen |
3 Copyright 2000 TU Muenchen |
4 *) |
4 *) |
5 |
5 |
6 header {* Strong normalization for simply-typed lambda calculus *} |
6 section {* Strong normalization for simply-typed lambda calculus *} |
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 |