#
e60cf64d |
|
06-Jan-2019 |
wenzelm <none@none> |
isabelle update -u path_cartouches;
|
#
a4bab154 |
|
04-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
#
b55041ee |
|
04-Jul-2018 |
Lars Hupel <lars.hupel@mytum.de> |
avoid clashes in quickcheck [random]
|
#
a7ccdf43 |
|
10-Jan-2018 |
nipkow <none@none> |
ran isabelle update_op on all sources
|
#
3bed0df2 |
|
14-Apr-2016 |
wenzelm <none@none> |
misc tuning and standardization;
|
#
0df376fc |
|
07-Dec-2015 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
#
85ed9565 |
|
01-Sep-2015 |
wenzelm <none@none> |
eliminated \<Colon>;
|
#
1901affb |
|
18-Jul-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
#
0976a200 |
|
05-Dec-2014 |
haftmann <none@none> |
allow multiple inheritance of targets --HG-- extra : rebase_source : 9d4980222d189226728427249e77a98373cb2011
|
#
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
#
f9cb1a7a |
|
29-Oct-2014 |
wenzelm <none@none> |
modernized setup;
|
#
b0d7f95d |
|
19-Sep-2014 |
blanchet <none@none> |
made new 'primrec' bootstrapping-capable
|
#
1ba740de |
|
02-Sep-2014 |
blanchet <none@none> |
use 'datatype_new' in 'Main'
|
#
9250249f |
|
25-Jan-2014 |
haftmann <none@none> |
prefer explicit code symbol type over ad-hoc name mangling
|
#
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
|