changeset 59730 | b7c394c7a619 |
parent 58889 | 5b7a9633cfa8 |
child 61986 | 2461779da2b8 |
--- a/src/HOL/Proofs/Extraction/Util.thy Tue Mar 10 16:12:35 2015 +0000 +++ b/src/HOL/Proofs/Extraction/Util.thy Mon Mar 16 15:30:00 2015 +0000 @@ -5,7 +5,7 @@ section {* Auxiliary lemmas used in program extraction examples *} theory Util -imports Old_Datatype +imports "~~/src/HOL/Library/Old_Datatype" begin text {*