| #
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
|