# HG changeset patch
# User haftmann
# Date 1352759080 -3600
# Node ID 94041d602ecb32eae883ac642da111b3cfd0a7a5
# Parent  6da283e4497b9540a7410d43575fbfadcd4b0b8e
tuned import order

diff -r 6da283e4497b -r 94041d602ecb src/HOL/Code_Evaluation.thy
--- 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 *}
diff -r 6da283e4497b -r 94041d602ecb src/HOL/DSequence.thy
--- 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"
diff -r 6da283e4497b -r 94041d602ecb src/HOL/Lazy_Sequence.thy
--- 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"
diff -r 6da283e4497b -r 94041d602ecb src/HOL/New_DSequence.thy
--- 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 *}
diff -r 6da283e4497b -r 94041d602ecb src/HOL/New_Random_Sequence.thy
--- 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"
diff -r 6da283e4497b -r 94041d602ecb src/HOL/Predicate_Compile.thy
--- 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
 
diff -r 6da283e4497b -r 94041d602ecb src/HOL/Random_Sequence.thy
--- 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)"