# HG changeset patch
# User blanchet
# Date 1346167493 -7200
# Node ID debfa361f648e1aa63c2905c1eb528f68b950764
# Parent  b62d14275b89370cec4055e0c39f0613a1ebd42c
fixed import paths in examples

diff -r b62d14275b89 -r debfa361f648 src/HOL/Codatatype/Examples/HFset.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
 
 
diff -r b62d14275b89 -r debfa361f648 src/HOL/Codatatype/Examples/Lambda_Term.thy
--- 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
 
 
diff -r b62d14275b89 -r debfa361f648 src/HOL/Codatatype/Examples/ListF.thy
--- 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"
diff -r b62d14275b89 -r debfa361f648 src/HOL/Codatatype/Examples/Misc_Codata.thy
--- 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 *}
diff -r b62d14275b89 -r debfa361f648 src/HOL/Codatatype/Examples/Misc_Data.thy
--- 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 *}
diff -r b62d14275b89 -r debfa361f648 src/HOL/Codatatype/Examples/Process.thy
--- 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"
diff -r b62d14275b89 -r debfa361f648 src/HOL/Codatatype/Examples/TreeFsetI.thy
--- 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