--- 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