--- a/src/HOL/Code_Evaluation.thy Mon Nov 12 18:42:49 2012 +0100
+++ b/src/HOL/Code_Evaluation.thy Mon Nov 12 23:24:40 2012 +0100
@@ -5,7 +5,7 @@
header {* Term evaluation using the generic code generator *}
theory Code_Evaluation
-imports Plain Typerep Code_Numeral Predicate
+imports Plain Typerep New_DSequence
begin
subsection {* Term representation *}
--- a/src/HOL/DSequence.thy Mon Nov 12 18:42:49 2012 +0100
+++ b/src/HOL/DSequence.thy Mon Nov 12 23:24:40 2012 +0100
@@ -4,7 +4,7 @@
header {* Depth-Limited Sequences with failure element *}
theory DSequence
-imports Lazy_Sequence Code_Numeral
+imports Lazy_Sequence
begin
type_synonym 'a dseq = "code_numeral => bool => 'a Lazy_Sequence.lazy_sequence option"
--- a/src/HOL/Lazy_Sequence.thy Mon Nov 12 18:42:49 2012 +0100
+++ b/src/HOL/Lazy_Sequence.thy Mon Nov 12 23:24:40 2012 +0100
@@ -4,7 +4,7 @@
header {* Lazy sequences *}
theory Lazy_Sequence
-imports List Code_Numeral
+imports Predicate
begin
datatype 'a lazy_sequence = Empty | Insert 'a "'a lazy_sequence"
--- a/src/HOL/New_DSequence.thy Mon Nov 12 18:42:49 2012 +0100
+++ b/src/HOL/New_DSequence.thy Mon Nov 12 23:24:40 2012 +0100
@@ -4,7 +4,7 @@
header {* Depth-Limited Sequences with failure element *}
theory New_DSequence
-imports Random_Sequence
+imports DSequence
begin
subsection {* Positive Depth-Limited Sequence *}
--- a/src/HOL/New_Random_Sequence.thy Mon Nov 12 18:42:49 2012 +0100
+++ b/src/HOL/New_Random_Sequence.thy Mon Nov 12 23:24:40 2012 +0100
@@ -2,7 +2,7 @@
(* Author: Lukas Bulwahn, TU Muenchen *)
theory New_Random_Sequence
-imports Quickcheck New_DSequence
+imports Random_Sequence
begin
type_synonym 'a pos_random_dseq = "code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> 'a New_DSequence.pos_dseq"
--- a/src/HOL/Predicate_Compile.thy Mon Nov 12 18:42:49 2012 +0100
+++ b/src/HOL/Predicate_Compile.thy Mon Nov 12 23:24:40 2012 +0100
@@ -5,7 +5,7 @@
header {* A compiler for predicates defined by introduction rules *}
theory Predicate_Compile
-imports Predicate New_Random_Sequence Quickcheck_Exhaustive
+imports New_Random_Sequence Quickcheck_Exhaustive
keywords "code_pred" :: thy_goal and "values" :: diag
begin
--- a/src/HOL/Random_Sequence.thy Mon Nov 12 18:42:49 2012 +0100
+++ b/src/HOL/Random_Sequence.thy Mon Nov 12 23:24:40 2012 +0100
@@ -2,7 +2,7 @@
(* Author: Lukas Bulwahn, TU Muenchen *)
theory Random_Sequence
-imports Quickcheck DSequence
+imports Quickcheck
begin
type_synonym 'a random_dseq = "code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a DSequence.dseq \<times> Random.seed)"