| changeset 58382 | 2ee61d28c667 |
| parent 56073 | 29e308b56d23 |
| child 58622 | aa99568f56de |
--- a/src/HOL/Proofs/Lambda/WeakNorm.thy Thu Sep 18 18:49:58 2014 +0200 +++ b/src/HOL/Proofs/Lambda/WeakNorm.thy Thu Sep 18 19:01:50 2014 +0200 @@ -6,7 +6,8 @@ header {* Weak normalization for simply-typed lambda calculus *} theory WeakNorm -imports LambdaType NormalForm "~~/src/HOL/Library/Code_Target_Int" +imports LambdaType NormalForm "~~/src/HOL/Library/Old_Datatype" + "~~/src/HOL/Library/Code_Target_Int" begin text {*