#
e60cf64d |
|
06-Jan-2019 |
wenzelm <none@none> |
isabelle update -u path_cartouches;
|
#
3a4a7136 |
|
24-Apr-2018 |
haftmann <none@none> |
proper datatype for 8-bit characters
|
#
7f03ed51 |
|
07-Jan-2018 |
wenzelm <none@none> |
prefer formal comments;
|
#
c7cc1919 |
|
26-Nov-2017 |
wenzelm <none@none> |
more symbols;
|
#
bf0a2cfd |
|
14-Nov-2017 |
Lars Hupel <lars.hupel@mytum.de> |
instantiation char :: full_exhaustive by Andreas Lochbihler --HG-- extra : amend_source : 549e6f93c390b168c9df6bea73f7e912ca9ba985
|
#
e0d246a1 |
|
29-May-2017 |
eberlm <eberlm@in.tum.de> |
reorganised material on sublists --HG-- rename : src/HOL/Library/Sublist_Order.thy => src/HOL/Library/Subseq_Order.thy extra : amend_source : e295fcfca4d0d9db4c5591741cb62b62bb340c87
|
#
1577f9b6 |
|
23-Dec-2016 |
haftmann <none@none> |
restored instance for char, which got ancidentally lost in b3f2b8c906a6 --HG-- extra : rebase_source : e4251be5b8a732dcb59f4230e3b4ed182b604a55
|
#
3bed0df2 |
|
14-Apr-2016 |
wenzelm <none@none> |
misc tuning and standardization;
|
#
8175ce0f |
|
12-Mar-2016 |
haftmann <none@none> |
model characters directly as range 0..255 * * * operate on syntax terms rather than asts
|
#
204908bc |
|
18-Feb-2016 |
haftmann <none@none> |
more direct bootstrap of char type, still retaining the nibble representation for syntax --HG-- extra : rebase_source : fd206c5addb099b720d632a7511e1485f7f64874
|
#
952abf53 |
|
06-Sep-2015 |
wenzelm <none@none> |
do not expose low-level "_def" facts of 'function' definitions, to avoid potential confusion with the situation of plain 'definition';
|
#
1901affb |
|
18-Jul-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
#
103d949b |
|
05-Feb-2015 |
haftmann <none@none> |
slightly more standard code setup for String.literal, with explicit special case in predicate compiler
|
#
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
#
f9cb1a7a |
|
29-Oct-2014 |
wenzelm <none@none> |
modernized setup;
|
#
ae3211cd |
|
29-Oct-2014 |
wenzelm <none@none> |
tuned;
|
#
1e04f9e5 |
|
16-Sep-2014 |
blanchet <none@none> |
added 'extraction' plugins -- this might help 'HOL-Proofs'
|
#
3c8247b0 |
|
14-Sep-2014 |
blanchet <none@none> |
disable datatype 'plugins' for internal types
|
#
5fc26177 |
|
11-Sep-2014 |
blanchet <none@none> |
updated news
|
#
1ba740de |
|
02-Sep-2014 |
blanchet <none@none> |
use 'datatype_new' in 'Main'
|
#
06329277 |
|
13-Aug-2013 |
wenzelm <none@none> |
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
|
#
a7b3de52 |
|
23-Jun-2013 |
haftmann <none@none> |
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier --HG-- extra : rebase_source : ff8027ac9606264aa4b2d4f8da037c426a3db98b
|
#
5a8927d0 |
|
15-Feb-2013 |
haftmann <none@none> |
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
|
#
8e65386b |
|
14-Feb-2013 |
haftmann <none@none> |
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
|
#
bbf74aa0 |
|
20-Oct-2012 |
haftmann <none@none> |
moved quite generic material from theory Enum to more appropriate places --HG-- extra : rebase_source : aada8b3ff46b715201e6ecbb53f390c25461ebd9
|
#
e3227796 |
|
22-Aug-2012 |
wenzelm <none@none> |
prefer ML_file over old uses;
|
#
2d32b2fb |
|
30-Mar-2012 |
bulwahn <none@none> |
hiding fact not so aggressively
|
#
870593bf |
|
15-Mar-2012 |
wenzelm <none@none> |
declare command keywords via theory header, including strict checking outside Pure;
|
#
f7bf9ec6 |
|
05-Feb-2012 |
bulwahn <none@none> |
beautifying definitions of check_all and adding instance for finite_4
|
#
5ef0982a |
|
23-Jan-2012 |
bulwahn <none@none> |
random instance for sets
|
#
a8627fb8 |
|
20-Jan-2012 |
bulwahn <none@none> |
shortened definitions by adding some termify constants
|
#
8a1d6e8b |
|
20-Jan-2012 |
bulwahn <none@none> |
adding check_all instance for sets; tuned
|
#
75bb4731 |
|
12-Jan-2012 |
bulwahn <none@none> |
adding exhaustive instances for type constructor set
|
#
beae54df |
|
20-Dec-2011 |
bulwahn <none@none> |
quickcheck generators for abstract types; tuned
|
#
73beb7c3 |
|
12-Dec-2011 |
bulwahn <none@none> |
hiding constants and facts in the Quickcheck_Exhaustive and Quickcheck_Narrowing theory;
|
#
42d69caa |
|
04-Dec-2011 |
bulwahn <none@none> |
adding genuine flag to predicate_compile_quickcheck and prolog_quickcheck (cf. 5e46c225370e); adjusting smart quickcheck compilation to new signature of exhaustive generators (cf. 1f5fc44254d7);
|
#
ecce798a |
|
01-Dec-2011 |
bulwahn <none@none> |
hiding internal constants and facts more properly
|
#
39cfce84 |
|
01-Dec-2011 |
bulwahn <none@none> |
removing catch_match' now that catch_match is polymorphic
|
#
18003355 |
|
01-Dec-2011 |
bulwahn <none@none> |
the simple exhaustive compilation also indicates if counterexample is potentially spurious;
|
#
f76bb9be |
|
01-Dec-2011 |
bulwahn <none@none> |
changing the exhaustive generator signatures; replacing the hard-wired result type by its own identifier
|
#
bd993364 |
|
01-Dec-2011 |
bulwahn <none@none> |
quickcheck random can also find potential counterexamples; moved catch_match definition; split quickcheck setup;
|
#
893e30e8 |
|
30-Nov-2011 |
bulwahn <none@none> |
more stable introduction of the internally used unknown term
|
#
d316ac9e |
|
30-Nov-2011 |
bulwahn <none@none> |
adding a exception-safe term reification step in quickcheck; adding examples
|
#
a7a38059 |
|
11-Nov-2011 |
bulwahn <none@none> |
adding CPS compilation to predicate compiler; removing function_flattening reference; new testers smart_exhaustive and smart_slow_exhaustive; renaming PredicateCompFuns to Predicate_Comp_Funs;
|
#
83cf0d9f |
|
18-Jul-2011 |
bulwahn <none@none> |
renaming quickcheck_tester to quickcheck_batch_tester; tuned
|
#
98878c02 |
|
08-Apr-2011 |
bulwahn <none@none> |
splitting exhaustive and full_exhaustive into separate type classes
|
#
8dd54176 |
|
08-Apr-2011 |
bulwahn <none@none> |
theory definitions for fast exhaustive quickcheck compilation
|
#
5680c0aa |
|
08-Apr-2011 |
bulwahn <none@none> |
new compilation for exhaustive quickcheck
|
#
9dab5728 |
|
07-Apr-2011 |
bulwahn <none@none> |
removing instantiation exhaustive for unit in Quickcheck_Exhaustive
|
#
59690dc2 |
|
05-Apr-2011 |
bulwahn <none@none> |
deriving bounded_forall instances in quickcheck_exhaustive
|
#
7990ed92 |
|
01-Apr-2011 |
bulwahn <none@none> |
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
|
#
a908f44b |
|
25-Mar-2011 |
bulwahn <none@none> |
changing iteration scheme of functions to use minimal number of function updates for exhaustive testing
|
#
8284061e |
|
11-Mar-2011 |
bulwahn <none@none> |
moving exhaustive_generators.ML to Quickcheck directory --HG-- rename : src/HOL/Tools/exhaustive_generators.ML => src/HOL/Tools/Quickcheck/exhaustive_generators.ML
|
#
e3099591 |
|
11-Mar-2011 |
bulwahn <none@none> |
replacing naming of small by exhaustive
|
#
131e1c6a |
|
11-Mar-2011 |
bulwahn <none@none> |
renaming constants in Quickcheck_Exhaustive theory
|
#
7ee78d02 |
|
11-Mar-2011 |
bulwahn <none@none> |
renaming Smallcheck to Quickcheck_Exhaustive --HG-- rename : src/HOL/Smallcheck.thy => src/HOL/Quickcheck_Exhaustive.thy
|