changeset 66258 | 2b83dd24b301 |
parent 63361 | d10eab0672f9 |
--- a/src/HOL/Proofs/Extraction/Util.thy Sat Jul 08 17:33:11 2017 +0200 +++ b/src/HOL/Proofs/Extraction/Util.thy Sat Jul 08 19:34:46 2017 +0200 @@ -5,7 +5,7 @@ section \<open>Auxiliary lemmas used in program extraction examples\<close> theory Util -imports "~~/src/HOL/Library/Old_Datatype" +imports Main begin text \<open>Decidability of equality on natural numbers.\<close>