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.
Sun, 11 Dec 2011 21:57:22 +0100 huffman fix spelling
Sun, 11 Dec 2011 21:54:20 +0100 huffman fix spelling
Sun, 11 Dec 2011 18:22:06 +0100 nipkow added IMP/Live_True.thy
Sun, 11 Dec 2011 09:55:57 +0100 huffman replace many uses of 'lemmas' with 'lemma';
Sat, 10 Dec 2011 22:00:42 +0100 huffman prove class instances without extra lemmas
Sat, 10 Dec 2011 21:48:16 +0100 huffman finite class instance for word type; remove unused lemmas
Sat, 10 Dec 2011 21:07:59 +0100 huffman remove unused lemmas
Sat, 10 Dec 2011 16:24:22 +0100 huffman generalize some lemmas
Sat, 10 Dec 2011 13:00:58 +0100 huffman merged
Sat, 10 Dec 2011 08:29:19 +0100 huffman tidied Word.thy;
Fri, 09 Dec 2011 14:52:51 +0100 huffman remove redundant lemma word_diff_minus
Fri, 09 Dec 2011 14:14:05 +0100 huffman remove some duplicate lemmas, simplify some proofs
Fri, 09 Dec 2011 18:07:04 +0100 kuncar Quotient_Info stores only relation maps
Fri, 09 Dec 2011 16:08:32 +0100 bulwahn hiding definitional facts in Quickcheck; introducing catch_match more honestly
Fri, 09 Dec 2011 14:46:18 +0100 kuncar added dependencies
Fri, 09 Dec 2011 14:22:05 +0100 kuncar added an example file with lifting of constants with contravariant and co/contravariant types
Fri, 09 Dec 2011 14:16:42 +0100 kuncar merged
Fri, 09 Dec 2011 14:14:37 +0100 kuncar make ctxt the first parameter
Fri, 09 Dec 2011 14:12:02 +0100 kuncar context/theory parametres tuned
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
Fri, 09 Dec 2011 13:42:16 +0100 huffman add induction rule for list_all2
Fri, 09 Dec 2011 12:21:03 +0100 bulwahn deactivating quickcheck_narrowing if Efficient_Nat theory is loaded
Fri, 09 Dec 2011 12:21:01 +0100 bulwahn tuned quickcheck's response
Fri, 09 Dec 2011 11:31:13 +0100 noschinl more systematic lemma name
Thu, 08 Dec 2011 13:53:28 +0100 bulwahn adding examples for quickcheck narrowing about partial functions
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
Thu, 08 Dec 2011 13:46:04 +0100 huffman HOLCF/ex/Letrec.thy: keep class 'domain' as default sort
Thu, 08 Dec 2011 13:25:54 +0100 huffman more error checking for fixrec
Thu, 08 Dec 2011 13:25:40 +0100 huffman reinstate old functions cfst and csnd as abbreviations
Thu, 08 Dec 2011 09:10:54 +0100 nipkow merged
Thu, 08 Dec 2011 09:10:44 +0100 nipkow tuned
Wed, 07 Dec 2011 16:06:08 +0000 Christian Urban merged
Wed, 07 Dec 2011 14:00:02 +0000 Christian Urban added a specific tactic and method that deal with partial equivalence relations
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
Wed, 07 Dec 2011 16:03:05 +0100 blanchet avoid multiple TFF1 declarations
Wed, 07 Dec 2011 16:03:05 +0100 blanchet updated TFF1 support
Wed, 07 Dec 2011 16:03:05 +0100 blanchet updated Metis to 20110926 version
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
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
Wed, 07 Dec 2011 10:50:30 +0100 huffman add cancellation simprocs for type enat
Wed, 07 Dec 2011 11:24:45 +0100 nipkow tuned
Tue, 06 Dec 2011 15:23:16 +0100 bulwahn increasing quickcheck's timeout in the example theory to avoid failures on the testing infrastructure
Tue, 06 Dec 2011 14:29:37 +0100 hoelzl tuned proofs
Tue, 06 Dec 2011 14:18:24 +0100 nipkow added lemmas
Mon, 05 Dec 2011 22:29:43 +0100 nipkow tuned proof
Mon, 05 Dec 2011 17:33:57 +0100 hoelzl real is better supported than real_of_nat, use it in the nat => ereal coercion
Mon, 05 Dec 2011 14:47:01 +0100 kuncar merged
Mon, 05 Dec 2011 14:44:46 +0100 kuncar the note about morphisms moved in the description part
Mon, 05 Dec 2011 12:36:28 +0100 bulwahn updating documentation about quiet and verbose options in quickcheck
Mon, 05 Dec 2011 12:36:22 +0100 bulwahn making the default behaviour of quickcheck a little bit less verbose;
Mon, 05 Dec 2011 12:36:21 +0100 bulwahn adding verbose configuration to quickcheck
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
Mon, 05 Dec 2011 12:36:19 +0100 bulwahn the reporting random testing also returns if the counterexample is genuine or potentially spurious
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
Mon, 05 Dec 2011 12:36:05 +0100 bulwahn inverted flag potential to genuine_only in the quickcheck narrowing Haskell code
Mon, 05 Dec 2011 12:36:03 +0100 bulwahn NEWS
Mon, 05 Dec 2011 12:36:02 +0100 bulwahn documenting the genuine_only option in quickcheck;
Mon, 05 Dec 2011 12:36:00 +0100 bulwahn renaming potential flag to genuine_only flag with an inverse semantics
Mon, 05 Dec 2011 12:35:58 +0100 bulwahn quickcheck narrowing continues searching after found a potentially spurious counterexample
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip