| changeset 58372 | bfd497f2f4c2 |
| parent 58358 | cdce4471d590 |
| child 58392 | 00f5b1efc741 |
--- a/src/HOL/Datatype_Examples/Compat.thy Thu Sep 18 16:47:40 2014 +0200 +++ b/src/HOL/Datatype_Examples/Compat.thy Thu Sep 18 16:47:40 2014 +0200 @@ -8,7 +8,7 @@ header {* Tests for Compatibility with the Old Datatype Package *} theory Compat -imports Main +imports "~~/src/HOL/Library/Old_Datatype" begin subsection {* Viewing and Registering New-Style Datatypes as Old-Style Ones *}