changeset 49878 | 8ce596cae2a3 |
parent 49877 | b75555ec30a4 |
child 49880 | d7917ec16288 |
--- a/src/HOL/BNF/Examples/Derivation_Trees/Prelim.thy Tue Oct 16 17:08:20 2012 +0200 +++ b/src/HOL/BNF/Examples/Derivation_Trees/Prelim.thy Tue Oct 16 17:33:08 2012 +0200 @@ -8,7 +8,7 @@ header {* Preliminaries *} theory Prelim -imports "../../BNF" +imports "../../BNF" "../../More_BNFs" begin declare fset_to_fset[simp]