# 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 \ code_numeral \ Random.seed \ '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 \ code_numeral \ Random.seed \ ('a DSequence.dseq \ Random.seed)"