| Wed, 21 Dec 2011 15:04:28 +0100 |
blanchet |
treat polymorphic constructors specially in @? encodings
|
changeset |
files
|
| Wed, 21 Dec 2011 15:04:28 +0100 |
blanchet |
tuning
|
changeset |
files
|
| Wed, 21 Dec 2011 15:04:28 +0100 |
blanchet |
no need for type arguments for monomorphic constructors of polymorphic datatypes (e.g. "Nil")
|
changeset |
files
|
| Wed, 21 Dec 2011 14:38:21 +0100 |
bulwahn |
added some basic documentation about method induction_schema extracted from old NEWS
|
changeset |
files
|
| Wed, 21 Dec 2011 14:24:29 +0100 |
bulwahn |
adding documentation about the quickcheck_generator command in the IsarRef
|
changeset |
files
|
| Wed, 21 Dec 2011 09:41:16 +0100 |
bulwahn |
extending quickcheck example
|
changeset |
files
|
| Wed, 21 Dec 2011 09:39:14 +0100 |
bulwahn |
NEWS
|
changeset |
files
|
| Wed, 21 Dec 2011 09:21:35 +0100 |
bulwahn |
quickcheck_generator command also creates random generators
|
changeset |
files
|
| Tue, 20 Dec 2011 18:59:50 +0100 |
blanchet |
don't try to avoid SPASS keywords; instead, just suffix an underscore to all generated identifiers
|
changeset |
files
|
| Tue, 20 Dec 2011 18:59:50 +0100 |
blanchet |
one more SPASS identifier
|
changeset |
files
|
| Tue, 20 Dec 2011 18:59:46 +0100 |
blanchet |
tuning
|
changeset |
files
|
| Tue, 20 Dec 2011 18:46:05 +0100 |
noschinl |
merged
|
changeset |
files
|
| Sat, 17 Dec 2011 15:53:58 +0100 |
traytel |
meaningful error message on failing merges of coercion tables
|
changeset |
files
|
| Tue, 20 Dec 2011 11:40:56 +0100 |
noschinl |
add simp rules for enat and ereal
|
changeset |
files
|
| Mon, 19 Dec 2011 14:41:08 +0100 |
noschinl |
add lemmas
|
changeset |
files
|
| Mon, 19 Dec 2011 14:41:08 +0100 |
noschinl |
add lemmas
|
changeset |
files
|
| Mon, 19 Dec 2011 14:41:08 +0100 |
noschinl |
weaken preconditions on lemmas
|
changeset |
files
|
| Mon, 19 Dec 2011 14:41:08 +0100 |
noschinl |
add lemmas
|
changeset |
files
|
| Tue, 20 Dec 2011 17:40:21 +0100 |
bulwahn |
removing some debug output in quotient_definition
|
changeset |
files
|
| Tue, 20 Dec 2011 17:40:18 +0100 |
bulwahn |
adding quickcheck generators in some HOL-Library theories
|
changeset |
files
|
| Tue, 20 Dec 2011 17:40:17 +0100 |
bulwahn |
adding quickcheck generator for distinct lists; adding examples
|
changeset |
files
|
| Tue, 20 Dec 2011 17:40:15 +0100 |
bulwahn |
added keywords
|
changeset |
files
|
| Tue, 20 Dec 2011 17:39:56 +0100 |
bulwahn |
quickcheck generators for abstract types; tuned
|
changeset |
files
|
| Tue, 20 Dec 2011 17:22:31 +0100 |
bulwahn |
exporting instantiation functions in quickcheck for their usage in abstract generators
|
changeset |
files
|
| Tue, 20 Dec 2011 17:22:31 +0100 |
bulwahn |
generalize ensure_sort_datatype to ensure_sort in quickcheck_common to allow generators for abstract types;
|
changeset |
files
|
| Tue, 20 Dec 2011 14:43:42 +0100 |
bulwahn |
tuned
|
changeset |
files
|
| Tue, 20 Dec 2011 14:43:41 +0100 |
bulwahn |
tuned
|
changeset |
files
|
| Tue, 20 Dec 2011 13:04:46 +0100 |
blanchet |
ensure TPTP FOF/TFF/THF formulas are close
|
changeset |
files
|
| Tue, 20 Dec 2011 10:42:33 +0100 |
nipkow |
tuned
|
changeset |
files
|
| Mon, 19 Dec 2011 17:10:53 +0100 |
nipkow |
merged
|
changeset |
files
|