| #
c7cc1919 |
|
26-Nov-2017 |
wenzelm <none@none> |
more symbols;
|
| #
1901affb |
|
18-Jul-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
| #
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
| #
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
|
| #
891cc9a4 |
|
12-Nov-2012 |
haftmann <none@none> |
tuned import order
|
| #
0d0a8a60 |
|
30-Mar-2011 |
bulwahn <none@none> |
renewing specifications in HOL: replacing types by type_synonym
|
| #
82fe7ca2 |
|
16-Apr-2010 |
wenzelm <none@none> |
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
|
| #
38c70ec2 |
|
20-Jan-2010 |
bulwahn <none@none> |
adopting Sequences
|
| #
2456c710 |
|
20-Jan-2010 |
bulwahn <none@none> |
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
|