isabelle update -u path_cartouches;

proper datatype for 8-bit characters

prefer formal comments;

more symbols;

instantiation char :: full_exhaustive by Andreas Lochbihler

--HG--
extra : amend_source : 549e6f93c390b168c9df6bea73f7e912ca9ba985

reorganised material on sublists

--HG--
rename : src/HOL/Library/Sublist_Order.thy => src/HOL/Library/Subseq_Order.thy
extra : amend_source : e295fcfca4d0d9db4c5591741cb62b62bb340c87

restored instance for char, which got ancidentally lost in b3f2b8c906a6

--HG--
extra : rebase_source : e4251be5b8a732dcb59f4230e3b4ed182b604a55

misc tuning and standardization;

model characters directly as range 0..255
* * *
operate on syntax terms rather than asts

more direct bootstrap of char type, still retaining the nibble representation for syntax

--HG--
extra : rebase_source : fd206c5addb099b720d632a7511e1485f7f64874

do not expose low-level "_def" facts of 'function' definitions, to avoid potential confusion with the situation of plain 'definition';

isabelle update_cartouches;

slightly more standard code setup for String.literal, with explicit special case in predicate compiler

modernized header uniformly as section;

modernized setup;

tuned;

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

disable datatype 'plugins' for internal types

updated news

use 'datatype_new' in 'Main'

standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;

migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier

--HG--
extra : rebase_source : ff8027ac9606264aa4b2d4f8da037c426a3db98b

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

moved quite generic material from theory Enum to more appropriate places

--HG--
extra : rebase_source : aada8b3ff46b715201e6ecbb53f390c25461ebd9

prefer ML_file over old uses;

hiding fact not so aggressively

declare command keywords via theory header, including strict checking outside Pure;

beautifying definitions of check_all and adding instance for finite_4

random instance for sets

shortened definitions by adding some termify constants

adding check_all instance for sets; tuned

adding exhaustive instances for type constructor set

quickcheck generators for abstract types; tuned

hiding constants and facts in the Quickcheck_Exhaustive and Quickcheck_Narrowing theory;

adding genuine flag to predicate_compile_quickcheck and prolog_quickcheck (cf. 5e46c225370e);
adjusting smart quickcheck compilation to new signature of exhaustive generators (cf. 1f5fc44254d7);

hiding internal constants and facts more properly

removing catch_match' now that catch_match is polymorphic

the simple exhaustive compilation also indicates if counterexample is potentially spurious;

changing the exhaustive generator signatures;
replacing the hard-wired result type by its own identifier

quickcheck random can also find potential counterexamples;
moved catch_match definition;
split quickcheck setup;

more stable introduction of the internally used unknown term

adding a exception-safe term reification step in quickcheck; adding examples

adding CPS compilation to predicate compiler;
removing function_flattening reference;
new testers smart_exhaustive and smart_slow_exhaustive;
renaming PredicateCompFuns to Predicate_Comp_Funs;

renaming quickcheck_tester to quickcheck_batch_tester; tuned

splitting exhaustive and full_exhaustive into separate type classes

theory definitions for fast exhaustive quickcheck compilation

new compilation for exhaustive quickcheck

removing instantiation exhaustive for unit in Quickcheck_Exhaustive

deriving bounded_forall instances in quickcheck_exhaustive

adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall

changing iteration scheme of functions to use minimal number of function updates for exhaustive testing

moving exhaustive_generators.ML to Quickcheck directory

--HG--
rename : src/HOL/Tools/exhaustive_generators.ML => src/HOL/Tools/Quickcheck/exhaustive_generators.ML

replacing naming of small by exhaustive

renaming constants in Quickcheck_Exhaustive theory

renaming Smallcheck to Quickcheck_Exhaustive

--HG--
rename : src/HOL/Smallcheck.thy => src/HOL/Quickcheck_Exhaustive.thy