# HG changeset patch
# User blanchet
# Date 1390238696 -3600
# Node ID 2b0b6f69b148f3ca104e79de29392105f67bce38
# Parent  9b96fb4c8cfd68d5efe7230eaa20fc49058ccb7a
rationalized dependencies

diff -r 9b96fb4c8cfd -r 2b0b6f69b148 src/HOL/BNF_Examples/Derivation_Trees/Gram_Lang.thy
--- a/src/HOL/BNF_Examples/Derivation_Trees/Gram_Lang.thy	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/BNF_Examples/Derivation_Trees/Gram_Lang.thy	Mon Jan 20 18:24:56 2014 +0100
@@ -8,7 +8,7 @@
 header {* Language of a Grammar *}
 
 theory Gram_Lang
-imports DTree
+imports DTree "~~/src/HOL/Library/Infinite_Set"
 begin
 
 
diff -r 9b96fb4c8cfd -r 2b0b6f69b148 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
@@ -8,7 +8,7 @@
 header {* Preliminaries *}
 
 theory Prelim
-imports "../../BNF" "../../More_BNFs"
+imports "../../BNF/More_BNFs"
 begin
 
 declare fset_to_fset[simp]