| #
3241d387 |
|
06-Jun-2018 |
nipkow <none@none> |
Keep filter input syntax
|
| #
e0e22efa |
|
22-May-2018 |
nipkow <none@none> |
First step to remove nonstandard "[x <- xs. P]" syntax: only input
--HG--
extra : amend_source : a2e6a2312b63a5ed1947d3302e43341c073c9f03
|
| #
131dfaff |
|
15-Sep-2016 |
nipkow <none@none> |
renamed listsum -> sum_list, listprod ~> prod_list
|
| #
07a7e7cf |
|
13-Mar-2016 |
haftmann <none@none> |
more theorems on orderings
--HG--
extra : rebase_source : 4e5a14cb68359f057eb65c380c103e23971ad09c
|
| #
0df376fc |
|
07-Dec-2015 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
| #
1901affb |
|
18-Jul-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
| #
13ddea91 |
|
26-Nov-2014 |
wenzelm <none@none> |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
| #
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
| #
d22c2cb6 |
|
31-Aug-2014 |
haftmann <none@none> |
separated listsum material
|
| #
2fde10a4 |
|
12-Jun-2014 |
blanchet <none@none> |
tuned dependencies
|
| #
7bce7b18 |
|
11-Jun-2014 |
blanchet <none@none> |
register record extensions as freely generated types
|
| #
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
|
| #
5ef0982a |
|
23-Jan-2012 |
bulwahn <none@none> |
random instance for sets
|
| #
15635718 |
|
13-Sep-2011 |
huffman <none@none> |
tuned proofs
|
| #
0d0a8a60 |
|
30-Mar-2011 |
bulwahn <none@none> |
renewing specifications in HOL: replacing types by type_synonym
|
| #
5b59da77 |
|
13-Sep-2010 |
nipkow <none@none> |
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
|
| #
bb8268b1 |
|
07-Sep-2010 |
nipkow <none@none> |
expand_fun_eq -> ext_iff
expand_set_eq -> set_ext_iff
Naming in line now with multisets
|
| #
8c105c87 |
|
09-Jul-2010 |
haftmann <none@none> |
nicer xsymbol syntax for fcomp and scomp
|
| #
00f0c1c7 |
|
29-Apr-2010 |
haftmann <none@none> |
make random engine persistent using code_reflect
|
| #
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;
|
| #
6d339a77 |
|
29-Mar-2010 |
bulwahn <none@none> |
adding values command for new monad; added new random monad compilation to predicate_compile_quickcheck
|
| #
0134ef39 |
|
19-Feb-2010 |
haftmann <none@none> |
hide fact range_def
|
| #
e1fcc6ca |
|
27-Oct-2009 |
haftmann <none@none> |
tuned
|
| #
1e5beb93 |
|
29-Sep-2009 |
wenzelm <none@none> |
explicit indication of Unsynchronized.ref;
|
| #
44a7485c |
|
15-Jun-2009 |
haftmann <none@none> |
where there is nothing, nothing can be hidden
|
| #
a70bc27f |
|
14-Jun-2009 |
haftmann <none@none> |
dropped select_default
|
| #
4fef65d6 |
|
27-May-2009 |
haftmann <none@none> |
added lemma select_weight_cons_zero
|
| #
a3c2121d |
|
26-May-2009 |
haftmann <none@none> |
dropped superfluos prefixes
|
| #
71924e3c |
|
19-May-2009 |
haftmann <none@none> |
String.literal replaces message_string, code_numeral replaces (code_)index
--HG--
rename : src/HOL/Code_Index.thy => src/HOL/Code_Numeral.thy
|
| #
34edb441 |
|
19-May-2009 |
haftmann <none@none> |
moved Code_Index, Random and Quickcheck before Main
|
| #
719b95b2 |
|
18-May-2009 |
haftmann <none@none> |
hide fact log_def -- should not shadow regular log definition
|
| #
011c72db |
|
16-May-2009 |
haftmann <none@none> |
experimental move of Quickcheck and related theories to HOL image
--HG--
rename : src/HOL/Library/Code_Index.thy => src/HOL/Code_Index.thy
rename : src/HOL/Library/Quickcheck.thy => src/HOL/Quickcheck.thy
rename : src/HOL/Library/Random.thy => src/HOL/Random.thy
|