| Sat, 10 Dec 2011 21:07:59 +0100 |
huffman |
remove unused lemmas
|
changeset |
files
|
| Sat, 10 Dec 2011 16:24:22 +0100 |
huffman |
generalize some lemmas
|
changeset |
files
|
| Sat, 10 Dec 2011 13:00:58 +0100 |
huffman |
merged
|
changeset |
files
|
| Sat, 10 Dec 2011 08:29:19 +0100 |
huffman |
tidied Word.thy;
|
changeset |
files
|
| Fri, 09 Dec 2011 14:52:51 +0100 |
huffman |
remove redundant lemma word_diff_minus
|
changeset |
files
|
| Fri, 09 Dec 2011 14:14:05 +0100 |
huffman |
remove some duplicate lemmas, simplify some proofs
|
changeset |
files
|
| Fri, 09 Dec 2011 18:07:04 +0100 |
kuncar |
Quotient_Info stores only relation maps
|
changeset |
files
|
| Fri, 09 Dec 2011 16:08:32 +0100 |
bulwahn |
hiding definitional facts in Quickcheck; introducing catch_match more honestly
|
changeset |
files
|
| Fri, 09 Dec 2011 14:46:18 +0100 |
kuncar |
added dependencies
|
changeset |
files
|
| Fri, 09 Dec 2011 14:22:05 +0100 |
kuncar |
added an example file with lifting of constants with contravariant and co/contravariant types
|
changeset |
files
|
| Fri, 09 Dec 2011 14:16:42 +0100 |
kuncar |
merged
|
changeset |
files
|
| Fri, 09 Dec 2011 14:14:37 +0100 |
kuncar |
make ctxt the first parameter
|
changeset |
files
|
| Fri, 09 Dec 2011 14:12:02 +0100 |
kuncar |
context/theory parametres tuned
|
changeset |
files
|
| Fri, 09 Dec 2011 14:03:17 +0100 |
kuncar |
maps are taken from enriched type infrastracture, rewritten lifting of constants, now we can lift even contravariant and co/contravariant types
|
changeset |
files
|
| Fri, 09 Dec 2011 13:42:16 +0100 |
huffman |
add induction rule for list_all2
|
changeset |
files
|
| Fri, 09 Dec 2011 12:21:03 +0100 |
bulwahn |
deactivating quickcheck_narrowing if Efficient_Nat theory is loaded
|
changeset |
files
|
| Fri, 09 Dec 2011 12:21:01 +0100 |
bulwahn |
tuned quickcheck's response
|
changeset |
files
|
| Fri, 09 Dec 2011 11:31:13 +0100 |
noschinl |
more systematic lemma name
|
changeset |
files
|
| Thu, 08 Dec 2011 13:53:28 +0100 |
bulwahn |
adding examples for quickcheck narrowing about partial functions
|
changeset |
files
|
| Thu, 08 Dec 2011 13:53:27 +0100 |
bulwahn |
removing special code generator setup for hd and last function because this causes problems with quickcheck narrowing as the Haskell Prelude functions throw errors that cannot be caught instead of PatternFail exceptions
|
changeset |
files
|
| Thu, 08 Dec 2011 13:46:04 +0100 |
huffman |
HOLCF/ex/Letrec.thy: keep class 'domain' as default sort
|
changeset |
files
|
| Thu, 08 Dec 2011 13:25:54 +0100 |
huffman |
more error checking for fixrec
|
changeset |
files
|
| Thu, 08 Dec 2011 13:25:40 +0100 |
huffman |
reinstate old functions cfst and csnd as abbreviations
|
changeset |
files
|
| Thu, 08 Dec 2011 09:10:54 +0100 |
nipkow |
merged
|
changeset |
files
|
| Thu, 08 Dec 2011 09:10:44 +0100 |
nipkow |
tuned
|
changeset |
files
|
| Wed, 07 Dec 2011 16:06:08 +0000 |
Christian Urban |
merged
|
changeset |
files
|
| Wed, 07 Dec 2011 14:00:02 +0000 |
Christian Urban |
added a specific tactic and method that deal with partial equivalence relations
|
changeset |
files
|
| Wed, 07 Dec 2011 16:03:05 +0100 |
blanchet |
use same order of facts for preplay as for actual reconstruction -- Metis sometimes exhibits very different timings depending on the order of the facts
|
changeset |
files
|
| Wed, 07 Dec 2011 16:03:05 +0100 |
blanchet |
avoid multiple TFF1 declarations
|
changeset |
files
|
| Wed, 07 Dec 2011 16:03:05 +0100 |
blanchet |
updated TFF1 support
|
changeset |
files
|
| Wed, 07 Dec 2011 16:03:05 +0100 |
blanchet |
updated Metis to 20110926 version
|
changeset |
files
|
| Wed, 07 Dec 2011 15:10:29 +0100 |
hoelzl |
remove unnecessary sublocale instantiations in HOL-Probability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space
|
changeset |
files
|
| Mon, 05 Dec 2011 15:10:15 +0100 |
huffman |
remove mem_(c)ball_0 and centre_in_(c)ball from simpset, as rules mem_(c)ball always match instead
|
changeset |
files
|
| Wed, 07 Dec 2011 10:50:30 +0100 |
huffman |
add cancellation simprocs for type enat
|
changeset |
files
|
| Wed, 07 Dec 2011 11:24:45 +0100 |
nipkow |
tuned
|
changeset |
files
|
| Tue, 06 Dec 2011 15:23:16 +0100 |
bulwahn |
increasing quickcheck's timeout in the example theory to avoid failures on the testing infrastructure
|
changeset |
files
|
| Tue, 06 Dec 2011 14:29:37 +0100 |
hoelzl |
tuned proofs
|
changeset |
files
|
| Tue, 06 Dec 2011 14:18:24 +0100 |
nipkow |
added lemmas
|
changeset |
files
|
| Mon, 05 Dec 2011 22:29:43 +0100 |
nipkow |
tuned proof
|
changeset |
files
|
| Mon, 05 Dec 2011 17:33:57 +0100 |
hoelzl |
real is better supported than real_of_nat, use it in the nat => ereal coercion
|
changeset |
files
|
| Mon, 05 Dec 2011 14:47:01 +0100 |
kuncar |
merged
|
changeset |
files
|
| Mon, 05 Dec 2011 14:44:46 +0100 |
kuncar |
the note about morphisms moved in the description part
|
changeset |
files
|
| Mon, 05 Dec 2011 12:36:28 +0100 |
bulwahn |
updating documentation about quiet and verbose options in quickcheck
|
changeset |
files
|
| Mon, 05 Dec 2011 12:36:22 +0100 |
bulwahn |
making the default behaviour of quickcheck a little bit less verbose;
|
changeset |
files
|
| Mon, 05 Dec 2011 12:36:21 +0100 |
bulwahn |
adding verbose configuration to quickcheck
|
changeset |
files
|
| Mon, 05 Dec 2011 12:36:20 +0100 |
bulwahn |
random reporting compilation returns if counterexample is genuine or potentially spurious, and takes genuine_only option as argument
|
changeset |
files
|
| Mon, 05 Dec 2011 12:36:19 +0100 |
bulwahn |
the reporting random testing also returns if the counterexample is genuine or potentially spurious
|
changeset |
files
|
| Mon, 05 Dec 2011 12:36:06 +0100 |
bulwahn |
exhaustive returns if a counterexample is genuine or potentially spurious in the presence of assumptions more correctly
|
changeset |
files
|
| Mon, 05 Dec 2011 12:36:05 +0100 |
bulwahn |
inverted flag potential to genuine_only in the quickcheck narrowing Haskell code
|
changeset |
files
|
| Mon, 05 Dec 2011 12:36:03 +0100 |
bulwahn |
NEWS
|
changeset |
files
|
| Mon, 05 Dec 2011 12:36:02 +0100 |
bulwahn |
documenting the genuine_only option in quickcheck;
|
changeset |
files
|
| Mon, 05 Dec 2011 12:36:00 +0100 |
bulwahn |
renaming potential flag to genuine_only flag with an inverse semantics
|
changeset |
files
|
| Mon, 05 Dec 2011 12:35:58 +0100 |
bulwahn |
quickcheck narrowing continues searching after found a potentially spurious counterexample
|
changeset |
files
|
| Mon, 05 Dec 2011 12:35:06 +0100 |
bulwahn |
outputing the potentially spurious counterexample and continue search
|
changeset |
files
|
| Mon, 05 Dec 2011 12:35:05 +0100 |
bulwahn |
dynamic genuine_flag in compilation of random and exhaustive
|
changeset |
files
|
| Mon, 05 Dec 2011 12:35:04 +0100 |
bulwahn |
indicating where the restart should occur; making safe_if dynamic
|
changeset |
files
|
| Mon, 05 Dec 2011 07:31:11 +0100 |
nipkow |
merged
|
changeset |
files
|
| Mon, 05 Dec 2011 07:31:00 +0100 |
nipkow |
enforce parantheses around SKIP {_}
|
changeset |
files
|
| Sun, 04 Dec 2011 20:05:08 +0100 |
bulwahn |
adding genuine flag to predicate_compile_quickcheck and prolog_quickcheck (cf. 5e46c225370e);
|
changeset |
files
|
| Sun, 04 Dec 2011 18:30:57 +0100 |
huffman |
merged
|
changeset |
files
|