changeset 66453 | cc19f7ca2ed6 |
parent 63167 | 0909deb8059b |
--- a/src/HOL/Datatype_Examples/Derivation_Trees/Prelim.thy Fri Aug 18 13:55:05 2017 +0200 +++ b/src/HOL/Datatype_Examples/Derivation_Trees/Prelim.thy Fri Aug 18 20:47:47 2017 +0200 @@ -8,7 +8,7 @@ section \<open>Preliminaries\<close> theory Prelim -imports "~~/src/HOL/Library/FSet" +imports "HOL-Library.FSet" begin notation BNF_Def.convol ("\<langle>(_,/ _)\<rangle>")