| Mon, 12 Dec 2011 20:28:19 +0100 |
nipkow |
tuned
|
changeset |
files
|
| Mon, 12 Dec 2011 23:05:21 +0100 |
wenzelm |
datatype dtyp with explicit sort information;
|
changeset |
files
|
| Mon, 12 Dec 2011 20:55:57 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Mon, 12 Dec 2011 19:47:50 +0100 |
wenzelm |
updated generated file;
|
changeset |
files
|
| Mon, 12 Dec 2011 17:22:48 +0100 |
bulwahn |
tuned quickcheck's response
|
changeset |
files
|
| Mon, 12 Dec 2011 13:45:54 +0100 |
bulwahn |
hiding constants and facts in the Quickcheck_Exhaustive and Quickcheck_Narrowing theory;
|
changeset |
files
|
| Mon, 12 Dec 2011 12:03:34 +0100 |
huffman |
merged
|
changeset |
files
|
| Mon, 12 Dec 2011 08:19:37 +0100 |
huffman |
replace more uses of 'lemmas' with explicit 'lemma';
|
changeset |
files
|
| Mon, 12 Dec 2011 15:32:54 +0900 |
Cezary Kaliszyk |
Add Quotient_Rat: an example of using the quotient package with partial equivalence relations, defining rational numbers.
|
changeset |
files
|
| Sun, 11 Dec 2011 21:57:22 +0100 |
huffman |
fix spelling
|
changeset |
files
|
| Sun, 11 Dec 2011 21:54:20 +0100 |
huffman |
fix spelling
|
changeset |
files
|
| Sun, 11 Dec 2011 18:22:06 +0100 |
nipkow |
added IMP/Live_True.thy
|
changeset |
files
|
| Sun, 11 Dec 2011 09:55:57 +0100 |
huffman |
replace many uses of 'lemmas' with 'lemma';
|
changeset |
files
|
| Sat, 10 Dec 2011 22:00:42 +0100 |
huffman |
prove class instances without extra lemmas
|
changeset |
files
|
| Sat, 10 Dec 2011 21:48:16 +0100 |
huffman |
finite class instance for word type; remove unused lemmas
|
changeset |
files
|
| 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
|