compile
authorblanchet
Mon Jan 20 18:24:56 2014 +0100 (2014-01-20)
changeset 550761e73e090a514
parent 55075 b3d0a02a756d
child 55077 4cf280104b85
compile
src/HOL/BNF_Examples/Lambda_Term.thy
src/HOL/BNF_Examples/ListF.thy
src/HOL/BNF_Examples/Misc_Codatatype.thy
src/HOL/BNF_Examples/Misc_Datatype.thy
src/HOL/BNF_Examples/Stream.thy
src/HOL/BNF_Examples/Stream_Processor.thy
src/HOL/BNF_Examples/TreeFsetI.thy
src/HOL/Library/BNF_Decl.thy
     1.1 --- a/src/HOL/BNF_Examples/Lambda_Term.thy	Mon Jan 20 18:24:56 2014 +0100
     1.2 +++ b/src/HOL/BNF_Examples/Lambda_Term.thy	Mon Jan 20 18:24:56 2014 +0100
     1.3 @@ -9,11 +9,9 @@
     1.4  header {* Lambda-Terms *}
     1.5  
     1.6  theory Lambda_Term
     1.7 -imports "../More_BNFs"
     1.8 +imports "~~/src/HOL/Library/More_BNFs"
     1.9  begin
    1.10  
    1.11 -thy_deps
    1.12 -
    1.13  section {* Datatype definition *}
    1.14  
    1.15  datatype_new 'a trm =
     2.1 --- a/src/HOL/BNF_Examples/ListF.thy	Mon Jan 20 18:24:56 2014 +0100
     2.2 +++ b/src/HOL/BNF_Examples/ListF.thy	Mon Jan 20 18:24:56 2014 +0100
     2.3 @@ -9,7 +9,7 @@
     2.4  header {* Finite Lists *}
     2.5  
     2.6  theory ListF
     2.7 -imports "../BNF"
     2.8 +imports Main
     2.9  begin
    2.10  
    2.11  datatype_new 'a listF (map: mapF rel: relF) =
     3.1 --- a/src/HOL/BNF_Examples/Misc_Codatatype.thy	Mon Jan 20 18:24:56 2014 +0100
     3.2 +++ b/src/HOL/BNF_Examples/Misc_Codatatype.thy	Mon Jan 20 18:24:56 2014 +0100
     3.3 @@ -10,7 +10,7 @@
     3.4  header {* Miscellaneous Codatatype Definitions *}
     3.5  
     3.6  theory Misc_Codatatype
     3.7 -imports More_BNFs
     3.8 +imports "~~/src/HOL/Library/More_BNFs"
     3.9  begin
    3.10  
    3.11  codatatype simple = X1 | X2 | X3 | X4
     4.1 --- a/src/HOL/BNF_Examples/Misc_Datatype.thy	Mon Jan 20 18:24:56 2014 +0100
     4.2 +++ b/src/HOL/BNF_Examples/Misc_Datatype.thy	Mon Jan 20 18:24:56 2014 +0100
     4.3 @@ -10,7 +10,7 @@
     4.4  header {* Miscellaneous Datatype Definitions *}
     4.5  
     4.6  theory Misc_Datatype
     4.7 -imports "../BNF"
     4.8 +imports "~~/src/HOL/Library/More_BNFs"
     4.9  begin
    4.10  
    4.11  datatype_new simple = X1 | X2 | X3 | X4
     5.1 --- a/src/HOL/BNF_Examples/Stream.thy	Mon Jan 20 18:24:56 2014 +0100
     5.2 +++ b/src/HOL/BNF_Examples/Stream.thy	Mon Jan 20 18:24:56 2014 +0100
     5.3 @@ -9,7 +9,7 @@
     5.4  header {* Infinite Streams *}
     5.5  
     5.6  theory Stream
     5.7 -imports "~~/Library/Nat_Bijection"
     5.8 +imports "~~/src/HOL/Library/Nat_Bijection"
     5.9  begin
    5.10  
    5.11  codatatype (sset: 'a) stream (map: smap rel: stream_all2) =
     6.1 --- a/src/HOL/BNF_Examples/Stream_Processor.thy	Mon Jan 20 18:24:56 2014 +0100
     6.2 +++ b/src/HOL/BNF_Examples/Stream_Processor.thy	Mon Jan 20 18:24:56 2014 +0100
     6.3 @@ -9,7 +9,7 @@
     6.4  header {* Stream Processors *}
     6.5  
     6.6  theory Stream_Processor
     6.7 -imports Stream "../BNF_Decl"
     6.8 +imports Stream "~~/src/HOL/Library/BNF_Decl"
     6.9  begin
    6.10  
    6.11  section {* Continuous Functions on Streams *}
     7.1 --- a/src/HOL/BNF_Examples/TreeFsetI.thy	Mon Jan 20 18:24:56 2014 +0100
     7.2 +++ b/src/HOL/BNF_Examples/TreeFsetI.thy	Mon Jan 20 18:24:56 2014 +0100
     7.3 @@ -9,7 +9,7 @@
     7.4  header {* Finitely Branching Possibly Infinite Trees, with Sets of Children *}
     7.5  
     7.6  theory TreeFsetI
     7.7 -imports "../BNF"
     7.8 +imports "~~/src/HOL/Library/More_BNFs"
     7.9  begin
    7.10  
    7.11  hide_fact (open) Lifting_Product.prod_rel_def
     8.1 --- a/src/HOL/Library/BNF_Decl.thy	Mon Jan 20 18:24:56 2014 +0100
     8.2 +++ b/src/HOL/Library/BNF_Decl.thy	Mon Jan 20 18:24:56 2014 +0100
     8.3 @@ -13,6 +13,6 @@
     8.4    "bnf_decl" :: thy_decl
     8.5  begin
     8.6  
     8.7 -ML_file "Tools/bnf_decl.ML"
     8.8 +ML_file "bnf_decl.ML"
     8.9  
    8.10  end