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