changeset 66453 | cc19f7ca2ed6 |
parent 64986 | b81a048960a3 |
child 69597 | ff784d5a5bfb |
--- a/src/HOL/Proofs/ex/XML_Data.thy Fri Aug 18 13:55:05 2017 +0200 +++ b/src/HOL/Proofs/ex/XML_Data.thy Fri Aug 18 20:47:47 2017 +0200 @@ -6,7 +6,7 @@ *) theory XML_Data - imports "~~/src/HOL/Isar_Examples/Drinker" + imports "HOL-Isar_Examples.Drinker" begin subsection \<open>Export and re-import of global proof terms\<close>