| Mon, 22 Nov 2010 10:41:56 +0100 |
bulwahn |
renaming quickcheck generator code to random
|
changeset |
files
|
| Mon, 22 Nov 2010 10:41:55 +0100 |
bulwahn |
ported sledgehammer_tactic to current development version
|
changeset |
files
|
| Mon, 22 Nov 2010 10:41:54 +0100 |
bulwahn |
adding dependencies to IsaMakefile; adding sledgehammer_tactic in Mirabelle_Test
|
changeset |
files
|
| Mon, 22 Nov 2010 10:41:53 +0100 |
bulwahn |
adding files to use sledgehammer as a tactic for non-interactive use
|
changeset |
files
|
| Mon, 22 Nov 2010 10:41:52 +0100 |
bulwahn |
adding birthday paradoxon from some abandoned drawer
|
changeset |
files
|
| Mon, 22 Nov 2010 10:41:51 +0100 |
bulwahn |
adding extensional function spaces to the FuncSet library theory
|
changeset |
files
|
| Mon, 22 Nov 2010 09:19:34 +0100 |
haftmann |
tuned
|
changeset |
files
|
| Mon, 22 Nov 2010 09:18:25 +0100 |
haftmann |
tuned
|
changeset |
files
|
| Sat, 20 Nov 2010 01:07:16 +0100 |
wenzelm |
updated explode vs. raw_explode;
|
changeset |
files
|
| Sat, 20 Nov 2010 00:53:26 +0100 |
wenzelm |
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
|
changeset |
files
|
| Fri, 19 Nov 2010 23:48:07 +0100 |
wenzelm |
total Symbol.explode (cf. 1050315f6ee2);
|
changeset |
files
|
| Fri, 19 Nov 2010 21:14:12 +0100 |
wenzelm |
do not export Thy_Load.required, to avoid confusion about the interface;
|
changeset |
files
|
| Fri, 19 Nov 2010 09:07:23 -0800 |
huffman |
merged
|
changeset |
files
|
| Wed, 17 Nov 2010 16:13:33 -0800 |
huffman |
declare adm_chfin [simp]
|
changeset |
files
|
| Wed, 17 Nov 2010 16:05:18 -0800 |
huffman |
add lemma cont_fun; remove unused lemma monofun_app
|
changeset |
files
|