diff -r 2b0b6f69b148 -r b3d0a02a756d src/HOL/BNF_Examples/Derivation_Trees/Prelim.thy --- a/src/HOL/BNF_Examples/Derivation_Trees/Prelim.thy Mon Jan 20 18:24:56 2014 +0100 +++ b/src/HOL/BNF_Examples/Derivation_Trees/Prelim.thy Mon Jan 20 18:24:56 2014 +0100 @@ -1,4 +1,4 @@ -(* Title: HOL/BNF/Examples/Derivation_Trees/Prelim.thy +(* Title: HOL/BNF_Examples/Derivation_Trees/Prelim.thy Author: Andrei Popescu, TU Muenchen Copyright 2012 @@ -8,7 +8,7 @@ header {* Preliminaries *} theory Prelim -imports "../../BNF/More_BNFs" +imports "~~/src/HOL/Library/More_BNFs" begin declare fset_to_fset[simp]