fixed import paths in examples
authorblanchet
Tue, 28 Aug 2012 17:24:53 +0200
changeset 48980 debfa361f648
parent 48979 b62d14275b89
child 48981 3517d6f50b12
fixed import paths in examples
src/HOL/Codatatype/Examples/HFset.thy
src/HOL/Codatatype/Examples/Lambda_Term.thy
src/HOL/Codatatype/Examples/ListF.thy
src/HOL/Codatatype/Examples/Misc_Codata.thy
src/HOL/Codatatype/Examples/Misc_Data.thy
src/HOL/Codatatype/Examples/Process.thy
src/HOL/Codatatype/Examples/TreeFsetI.thy
--- a/src/HOL/Codatatype/Examples/HFset.thy	Tue Aug 28 17:19:59 2012 +0200
+++ b/src/HOL/Codatatype/Examples/HFset.thy	Tue Aug 28 17:24:53 2012 +0200
@@ -8,7 +8,7 @@
 header {* Hereditary Sets *}
 
 theory HFset
-imports "../Codatatype/Codatatype"
+imports "../Codatatype"
 begin
 
 
--- a/src/HOL/Codatatype/Examples/Lambda_Term.thy	Tue Aug 28 17:19:59 2012 +0200
+++ b/src/HOL/Codatatype/Examples/Lambda_Term.thy	Tue Aug 28 17:24:53 2012 +0200
@@ -9,7 +9,7 @@
 header {* Lambda-Terms *}
 
 theory Lambda_Term
-imports "../Codatatype/Codatatype"
+imports "../Codatatype"
 begin
 
 
--- a/src/HOL/Codatatype/Examples/ListF.thy	Tue Aug 28 17:19:59 2012 +0200
+++ b/src/HOL/Codatatype/Examples/ListF.thy	Tue Aug 28 17:24:53 2012 +0200
@@ -9,7 +9,7 @@
 header {* Finite Lists *}
 
 theory ListF
-imports "../Codatatype/Codatatype"
+imports "../Codatatype"
 begin
 
 bnf_data listF: 'list = "unit + 'a \<times> 'list"
--- a/src/HOL/Codatatype/Examples/Misc_Codata.thy	Tue Aug 28 17:19:59 2012 +0200
+++ b/src/HOL/Codatatype/Examples/Misc_Codata.thy	Tue Aug 28 17:24:53 2012 +0200
@@ -9,7 +9,7 @@
 header {* Miscellaneous Codatatype Declarations *}
 
 theory Misc_Codata
-imports "../Codatatype/Codatatype"
+imports "../Codatatype"
 begin
 
 ML {* quick_and_dirty := false *}
--- a/src/HOL/Codatatype/Examples/Misc_Data.thy	Tue Aug 28 17:19:59 2012 +0200
+++ b/src/HOL/Codatatype/Examples/Misc_Data.thy	Tue Aug 28 17:24:53 2012 +0200
@@ -9,7 +9,7 @@
 header {* Miscellaneous Datatype Declarations *}
 
 theory Misc_Data
-imports "../Codatatype/Codatatype"
+imports "../Codatatype"
 begin
 
 ML {* quick_and_dirty := false *}
--- a/src/HOL/Codatatype/Examples/Process.thy	Tue Aug 28 17:19:59 2012 +0200
+++ b/src/HOL/Codatatype/Examples/Process.thy	Tue Aug 28 17:24:53 2012 +0200
@@ -8,7 +8,7 @@
 header {* Processes *}
 
 theory Process
-imports "../Codatatype/Codatatype"
+imports "../Codatatype"
 begin
 
 bnf_codata process: 'p = "'a * 'p + 'p * 'p"
--- a/src/HOL/Codatatype/Examples/TreeFsetI.thy	Tue Aug 28 17:19:59 2012 +0200
+++ b/src/HOL/Codatatype/Examples/TreeFsetI.thy	Tue Aug 28 17:24:53 2012 +0200
@@ -9,7 +9,7 @@
 header {* Finitely Branching Possibly Infinite Trees, with Sets of Children *}
 
 theory TreeFsetI
-imports "../Codatatype/Codatatype"
+imports "../Codatatype"
 begin
 
 definition pair_fun (infixr "\<odot>" 50) where