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