src/HOL/Lazy_Sequence.thy
2010-10-22 hoelzl 2010-10-22 Changed section title to please LaTeX.
2010-10-21 bulwahn 2010-10-21 added generator_dseq compilation for a sound depth-limited compilation with small value generators
2010-08-27 haftmann 2010-08-27 renamed class/constant eq to equal; tuned some instantiations
2010-05-12 huffman 2010-05-12 use 'subsection' instead of 'section', to maintain 1 chapter per file in generated document
2010-04-29 haftmann 2010-04-29 dropped unnecessary ML code
2010-04-28 haftmann 2010-04-28 export somehow odd mapa explicitly
2010-04-28 haftmann 2010-04-28 avoid code_datatype antiquotation
2010-04-16 wenzelm 2010-04-16 replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
2010-03-31 bulwahn 2010-03-31 adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
2010-03-29 bulwahn 2010-03-29 adding Lazy_Sequences with explicit depth-bound
2010-03-29 bulwahn 2010-03-29 removed yieldn in Lazy_Sequence and put in the ML structure; corrects behaviour of values command
2010-03-29 bulwahn 2010-03-29 adding values command for new monad; added new random monad compilation to predicate_compile_quickcheck
2010-01-22 bulwahn 2010-01-22 correctly hiding facts of Lazy_Sequence
2010-01-20 bulwahn 2010-01-20 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck