# HG changeset patch
# User blanchet
# Date 1390238696 -3600
# Node ID 1e73e090a514df8e6a2c597ebf841e16e291853b
# Parent  b3d0a02a756de5bd69d0727bb44824d3beecb4ba
compile

diff -r b3d0a02a756d -r 1e73e090a514 src/HOL/BNF_Examples/Lambda_Term.thy
--- a/src/HOL/BNF_Examples/Lambda_Term.thy	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/BNF_Examples/Lambda_Term.thy	Mon Jan 20 18:24:56 2014 +0100
@@ -9,11 +9,9 @@
 header {* Lambda-Terms *}
 
 theory Lambda_Term
-imports "../More_BNFs"
+imports "~~/src/HOL/Library/More_BNFs"
 begin
 
-thy_deps
-
 section {* Datatype definition *}
 
 datatype_new 'a trm =
diff -r b3d0a02a756d -r 1e73e090a514 src/HOL/BNF_Examples/ListF.thy
--- a/src/HOL/BNF_Examples/ListF.thy	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/BNF_Examples/ListF.thy	Mon Jan 20 18:24:56 2014 +0100
@@ -9,7 +9,7 @@
 header {* Finite Lists *}
 
 theory ListF
-imports "../BNF"
+imports Main
 begin
 
 datatype_new 'a listF (map: mapF rel: relF) =
diff -r b3d0a02a756d -r 1e73e090a514 src/HOL/BNF_Examples/Misc_Codatatype.thy
--- a/src/HOL/BNF_Examples/Misc_Codatatype.thy	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/BNF_Examples/Misc_Codatatype.thy	Mon Jan 20 18:24:56 2014 +0100
@@ -10,7 +10,7 @@
 header {* Miscellaneous Codatatype Definitions *}
 
 theory Misc_Codatatype
-imports More_BNFs
+imports "~~/src/HOL/Library/More_BNFs"
 begin
 
 codatatype simple = X1 | X2 | X3 | X4
diff -r b3d0a02a756d -r 1e73e090a514 src/HOL/BNF_Examples/Misc_Datatype.thy
--- a/src/HOL/BNF_Examples/Misc_Datatype.thy	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/BNF_Examples/Misc_Datatype.thy	Mon Jan 20 18:24:56 2014 +0100
@@ -10,7 +10,7 @@
 header {* Miscellaneous Datatype Definitions *}
 
 theory Misc_Datatype
-imports "../BNF"
+imports "~~/src/HOL/Library/More_BNFs"
 begin
 
 datatype_new simple = X1 | X2 | X3 | X4
diff -r b3d0a02a756d -r 1e73e090a514 src/HOL/BNF_Examples/Stream.thy
--- a/src/HOL/BNF_Examples/Stream.thy	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/BNF_Examples/Stream.thy	Mon Jan 20 18:24:56 2014 +0100
@@ -9,7 +9,7 @@
 header {* Infinite Streams *}
 
 theory Stream
-imports "~~/Library/Nat_Bijection"
+imports "~~/src/HOL/Library/Nat_Bijection"
 begin
 
 codatatype (sset: 'a) stream (map: smap rel: stream_all2) =
diff -r b3d0a02a756d -r 1e73e090a514 src/HOL/BNF_Examples/Stream_Processor.thy
--- a/src/HOL/BNF_Examples/Stream_Processor.thy	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/BNF_Examples/Stream_Processor.thy	Mon Jan 20 18:24:56 2014 +0100
@@ -9,7 +9,7 @@
 header {* Stream Processors *}
 
 theory Stream_Processor
-imports Stream "../BNF_Decl"
+imports Stream "~~/src/HOL/Library/BNF_Decl"
 begin
 
 section {* Continuous Functions on Streams *}
diff -r b3d0a02a756d -r 1e73e090a514 src/HOL/BNF_Examples/TreeFsetI.thy
--- a/src/HOL/BNF_Examples/TreeFsetI.thy	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/BNF_Examples/TreeFsetI.thy	Mon Jan 20 18:24:56 2014 +0100
@@ -9,7 +9,7 @@
 header {* Finitely Branching Possibly Infinite Trees, with Sets of Children *}
 
 theory TreeFsetI
-imports "../BNF"
+imports "~~/src/HOL/Library/More_BNFs"
 begin
 
 hide_fact (open) Lifting_Product.prod_rel_def
diff -r b3d0a02a756d -r 1e73e090a514 src/HOL/Library/BNF_Decl.thy
--- a/src/HOL/Library/BNF_Decl.thy	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/Library/BNF_Decl.thy	Mon Jan 20 18:24:56 2014 +0100
@@ -13,6 +13,6 @@
   "bnf_decl" :: thy_decl
 begin
 
-ML_file "Tools/bnf_decl.ML"
+ML_file "bnf_decl.ML"
 
 end