| changeset 65535 | 1bf7b5dc34c8 |
| parent 63060 | 293ede07b775 |
| child 67320 | 6afba546f0e5 |
--- a/src/HOL/Proofs/Lambda/WeakNorm.thy Fri Apr 21 15:26:24 2017 +0200 +++ b/src/HOL/Proofs/Lambda/WeakNorm.thy Fri Apr 21 16:12:11 2017 +0200 @@ -6,8 +6,7 @@ section \<open>Weak normalization for simply-typed lambda calculus\<close> theory WeakNorm -imports LambdaType NormalForm "~~/src/HOL/Library/Old_Datatype" - "~~/src/HOL/Library/Code_Target_Int" +imports LambdaType NormalForm "HOL-Library.Old_Datatype" "HOL-Library.Code_Target_Int" begin text \<open>