tuned import order
authorhaftmann
Mon Nov 12 23:24:40 2012 +0100 (2012-11-12)
changeset 5005594041d602ecb
parent 50054 6da283e4497b
child 50056 72efd6b4038d
tuned import order
src/HOL/Code_Evaluation.thy
src/HOL/DSequence.thy
src/HOL/Lazy_Sequence.thy
src/HOL/New_DSequence.thy
src/HOL/New_Random_Sequence.thy
src/HOL/Predicate_Compile.thy
src/HOL/Random_Sequence.thy
     1.1 --- a/src/HOL/Code_Evaluation.thy	Mon Nov 12 18:42:49 2012 +0100
     1.2 +++ b/src/HOL/Code_Evaluation.thy	Mon Nov 12 23:24:40 2012 +0100
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* Term evaluation using the generic code generator *}
     1.5  
     1.6  theory Code_Evaluation
     1.7 -imports Plain Typerep Code_Numeral Predicate
     1.8 +imports Plain Typerep New_DSequence
     1.9  begin
    1.10  
    1.11  subsection {* Term representation *}
     2.1 --- a/src/HOL/DSequence.thy	Mon Nov 12 18:42:49 2012 +0100
     2.2 +++ b/src/HOL/DSequence.thy	Mon Nov 12 23:24:40 2012 +0100
     2.3 @@ -4,7 +4,7 @@
     2.4  header {* Depth-Limited Sequences with failure element *}
     2.5  
     2.6  theory DSequence
     2.7 -imports Lazy_Sequence Code_Numeral
     2.8 +imports Lazy_Sequence
     2.9  begin
    2.10  
    2.11  type_synonym 'a dseq = "code_numeral => bool => 'a Lazy_Sequence.lazy_sequence option"
     3.1 --- a/src/HOL/Lazy_Sequence.thy	Mon Nov 12 18:42:49 2012 +0100
     3.2 +++ b/src/HOL/Lazy_Sequence.thy	Mon Nov 12 23:24:40 2012 +0100
     3.3 @@ -4,7 +4,7 @@
     3.4  header {* Lazy sequences *}
     3.5  
     3.6  theory Lazy_Sequence
     3.7 -imports List Code_Numeral
     3.8 +imports Predicate
     3.9  begin
    3.10  
    3.11  datatype 'a lazy_sequence = Empty | Insert 'a "'a lazy_sequence"
     4.1 --- a/src/HOL/New_DSequence.thy	Mon Nov 12 18:42:49 2012 +0100
     4.2 +++ b/src/HOL/New_DSequence.thy	Mon Nov 12 23:24:40 2012 +0100
     4.3 @@ -4,7 +4,7 @@
     4.4  header {* Depth-Limited Sequences with failure element *}
     4.5  
     4.6  theory New_DSequence
     4.7 -imports Random_Sequence
     4.8 +imports DSequence
     4.9  begin
    4.10  
    4.11  subsection {* Positive Depth-Limited Sequence *}
     5.1 --- a/src/HOL/New_Random_Sequence.thy	Mon Nov 12 18:42:49 2012 +0100
     5.2 +++ b/src/HOL/New_Random_Sequence.thy	Mon Nov 12 23:24:40 2012 +0100
     5.3 @@ -2,7 +2,7 @@
     5.4  (* Author: Lukas Bulwahn, TU Muenchen *)
     5.5  
     5.6  theory New_Random_Sequence
     5.7 -imports Quickcheck New_DSequence
     5.8 +imports Random_Sequence
     5.9  begin
    5.10  
    5.11  type_synonym 'a pos_random_dseq = "code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> 'a New_DSequence.pos_dseq"
     6.1 --- a/src/HOL/Predicate_Compile.thy	Mon Nov 12 18:42:49 2012 +0100
     6.2 +++ b/src/HOL/Predicate_Compile.thy	Mon Nov 12 23:24:40 2012 +0100
     6.3 @@ -5,7 +5,7 @@
     6.4  header {* A compiler for predicates defined by introduction rules *}
     6.5  
     6.6  theory Predicate_Compile
     6.7 -imports Predicate New_Random_Sequence Quickcheck_Exhaustive
     6.8 +imports New_Random_Sequence Quickcheck_Exhaustive
     6.9  keywords "code_pred" :: thy_goal and "values" :: diag
    6.10  begin
    6.11  
     7.1 --- a/src/HOL/Random_Sequence.thy	Mon Nov 12 18:42:49 2012 +0100
     7.2 +++ b/src/HOL/Random_Sequence.thy	Mon Nov 12 23:24:40 2012 +0100
     7.3 @@ -2,7 +2,7 @@
     7.4  (* Author: Lukas Bulwahn, TU Muenchen *)
     7.5  
     7.6  theory Random_Sequence
     7.7 -imports Quickcheck DSequence
     7.8 +imports Quickcheck
     7.9  begin
    7.10  
    7.11  type_synonym 'a random_dseq = "code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a DSequence.dseq \<times> Random.seed)"