# 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