isabelle update_cartouches;

modernized header uniformly as section;

added 'extraction' plugins -- this might help 'HOL-Proofs'

disable datatype 'plugins' for internal types

updated news

use 'datatype_new' in 'Main'

renamed 'xxx_size' to 'size_xxx' for old datatype package

move size hooks together, with new one preceding old one and sharing same theory data

adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'

merged 'Option.map' and 'Option.map_option'

adapted theories to 'xxx_case' to 'case_xxx'
* * *
'char_case' -> 'case_char' and same for 'rec'
* * *
compile
* * *
renamed 'xxx_case' to 'case_xxx'

adapted theories to '{case,rec}_{list,option}' names

two target language numeral types: integer and natural, as replacement for code_numeral;
former theory HOL/Library/Code_Numeral_Types replaces HOL/Code_Numeral;
refined stack of theories implementing int and/or nat by target language numerals;
reduced number of target language numeral types to exactly one

--HG--
extra : rebase_source : ffa0242ad108fe680ff144a716257c0784285d17

reform of predicate compiler / quickcheck theories:
implement yieldn operations uniformly on the ML level -- predicate compiler uses negative integers as parameter to yieldn, whereas code_numeral represents natural numbers!
avoid odd New_ prefix by joining related theories;
avoid overcompact name DSequence;
separated predicate inside random monad into separate theory;
consolidated name of theory Quickcheck

--HG--
rename : src/HOL/DSequence.thy => src/HOL/Limited_Sequence.thy
rename : src/HOL/Quickcheck.thy => src/HOL/Quickcheck_Random.thy
extra : rebase_source : b6adaac1637d6d1cc809d2f937ae890fcc21969c

tuned import order

modernizing predicate_compile_quickcheck

renewing specifications in HOL: replacing types by type_synonym

Changed section title to please LaTeX.

added generator_dseq compilation for a sound depth-limited compilation with small value generators

renamed class/constant eq to equal; tuned some instantiations

use 'subsection' instead of 'section', to maintain 1 chapter per file in generated document

dropped unnecessary ML code

export somehow odd mapa explicitly

avoid code_datatype antiquotation

replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;

adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler

adding Lazy_Sequences with explicit depth-bound

removed yieldn in Lazy_Sequence and put in the ML structure; corrects behaviour of values command

adding values command for new monad; added new random monad compilation to predicate_compile_quickcheck

correctly hiding facts of Lazy_Sequence

refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck