#
e60cf64d |
|
06-Jan-2019 |
wenzelm <none@none> |
isabelle update -u path_cartouches;
|
#
a4bab154 |
|
04-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
#
f5796e6d |
|
14-Feb-2018 |
wenzelm <none@none> |
more symbols;
|
#
2dc6f8f0 |
|
11-Jul-2016 |
wenzelm <none@none> |
tuned;
|
#
35f7dccd |
|
23-Feb-2016 |
nipkow <none@none> |
more canonical names
|
#
1901affb |
|
18-Jul-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
#
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
#
7420ab5c |
|
29-Oct-2014 |
wenzelm <none@none> |
modernized setup;
|
#
28f93e94 |
|
17-Feb-2014 |
wenzelm <none@none> |
more informative error;
|
#
ff3e7af5 |
|
16-May-2013 |
Andreas Lochbihler <none@none> |
setup for set membership as a predicate for code_pred
|
#
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
|
#
891cc9a4 |
|
12-Nov-2012 |
haftmann <none@none> |
tuned import order
|
#
e3227796 |
|
22-Aug-2012 |
wenzelm <none@none> |
prefer ML_file over old uses;
|
#
870593bf |
|
15-Mar-2012 |
wenzelm <none@none> |
declare command keywords via theory header, including strict checking outside Pure;
|
#
484c9d58 |
|
24-Feb-2012 |
haftmann <none@none> |
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy --HG-- extra : rebase_source : ed15629634477aff0a8efea30547f496c70907ad
|
#
37822d49 |
|
23-Feb-2012 |
haftmann <none@none> |
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
|
#
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;
|
#
053198db |
|
21-Oct-2010 |
bulwahn <none@none> |
splitting large core file into core_data, mode_inference and predicate_compile_proof
|
#
76764f94 |
|
31-Mar-2010 |
bulwahn <none@none> |
putting compilation setup of predicate compiler in a separate file
|
#
c68a8bbe |
|
29-Mar-2010 |
bulwahn <none@none> |
adding specialisation of predicates to the predicate compiler
|
#
38d0425b |
|
29-Mar-2010 |
bulwahn <none@none> |
adopting Predicate_Compile
|
#
679d966a |
|
22-Mar-2010 |
wenzelm <none@none> |
recovered header;
|
#
28c4a8f4 |
|
22-Mar-2010 |
bulwahn <none@none> |
removed unused Predicate_Compile_Set
|
#
b26806d3 |
|
22-Mar-2010 |
bulwahn <none@none> |
reviving the classical depth-limited computation in the predicate compiler
|
#
2456c710 |
|
20-Jan-2010 |
bulwahn <none@none> |
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
|
#
3a4c9852 |
|
27-Oct-2009 |
wenzelm <none@none> |
proper headers;
|
#
11ce0ee7 |
|
27-Oct-2009 |
bulwahn <none@none> |
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
|