Tue, 13 Dec 2011 14:55:42 +0100 blanchet added missing quantifier
Tue, 13 Dec 2011 14:55:42 +0100 blanchet remove needless declaration in TFF1 problems
Tue, 13 Dec 2011 14:55:42 +0100 blanchet correctly declare implicit TFF1 types that appear first as type arguments with "$tType" and not "$i
Tue, 13 Dec 2011 15:18:52 +0100 wenzelm modernized specifications;
Tue, 13 Dec 2011 14:04:20 +0100 kuncar support phantom types as quotient types
Mon, 12 Dec 2011 23:06:41 +0100 wenzelm merged
Mon, 12 Dec 2011 20:28:34 +0100 nipkow merged
Mon, 12 Dec 2011 20:28:19 +0100 nipkow tuned
Mon, 12 Dec 2011 23:05:21 +0100 wenzelm datatype dtyp with explicit sort information;
Mon, 12 Dec 2011 20:55:57 +0100 wenzelm tuned;
Mon, 12 Dec 2011 19:47:50 +0100 wenzelm updated generated file;
Mon, 12 Dec 2011 17:22:48 +0100 bulwahn tuned quickcheck's response
Mon, 12 Dec 2011 13:45:54 +0100 bulwahn hiding constants and facts in the Quickcheck_Exhaustive and Quickcheck_Narrowing theory;
Mon, 12 Dec 2011 12:03:34 +0100 huffman merged
Mon, 12 Dec 2011 08:19:37 +0100 huffman replace more uses of 'lemmas' with explicit 'lemma';
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
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip