| changeset 51143 | 0a2371e7ced3 |
| parent 50630 | 1ea90e8046dc |
| child 51272 | 9c8d63b4b6be |
--- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Fri Feb 15 08:31:30 2013 +0100 +++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Fri Feb 15 08:31:31 2013 +0100 @@ -5,7 +5,7 @@ header {* Linked Lists by ML references *} theory Linked_Lists -imports "../Imperative_HOL" "~~/src/HOL/Library/Code_Integer" +imports "../Imperative_HOL" "~~/src/HOL/Library/Code_Target_Int" begin section {* Definition of Linked Lists *}