kuncar [Fri, 09 Dec 2011 14:16:42 +0100] rev 45798
merged
kuncar [Fri, 09 Dec 2011 14:14:37 +0100] rev 45797
make ctxt the first parameter
kuncar [Fri, 09 Dec 2011 14:12:02 +0100] rev 45796
context/theory parametres tuned
kuncar [Fri, 09 Dec 2011 14:03:17 +0100] rev 45795
maps are taken from enriched type infrastracture, rewritten lifting of constants, now we can lift even contravariant and co/contravariant types
huffman [Fri, 09 Dec 2011 13:42:16 +0100] rev 45794
add induction rule for list_all2
bulwahn [Fri, 09 Dec 2011 12:21:03 +0100] rev 45793
deactivating quickcheck_narrowing if Efficient_Nat theory is loaded
bulwahn [Fri, 09 Dec 2011 12:21:01 +0100] rev 45792
tuned quickcheck's response
noschinl [Fri, 09 Dec 2011 11:31:13 +0100] rev 45791
more systematic lemma name
bulwahn [Thu, 08 Dec 2011 13:53:28 +0100] rev 45790
adding examples for quickcheck narrowing about partial functions
bulwahn [Thu, 08 Dec 2011 13:53:27 +0100] rev 45789
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
huffman [Thu, 08 Dec 2011 13:46:04 +0100] rev 45788
HOLCF/ex/Letrec.thy: keep class 'domain' as default sort
huffman [Thu, 08 Dec 2011 13:25:54 +0100] rev 45787
more error checking for fixrec
huffman [Thu, 08 Dec 2011 13:25:40 +0100] rev 45786
reinstate old functions cfst and csnd as abbreviations
nipkow [Thu, 08 Dec 2011 09:10:54 +0100] rev 45785
merged
nipkow [Thu, 08 Dec 2011 09:10:44 +0100] rev 45784
tuned
Christian Urban <urbanc@in.tum.de> [Wed, 07 Dec 2011 16:06:08 +0000] rev 45783
merged
Christian Urban <urbanc@in.tum.de> [Wed, 07 Dec 2011 14:00:02 +0000] rev 45782
added a specific tactic and method that deal with partial equivalence relations
blanchet [Wed, 07 Dec 2011 16:03:05 +0100] rev 45781
use same order of facts for preplay as for actual reconstruction -- Metis sometimes exhibits very different timings depending on the order of the facts
blanchet [Wed, 07 Dec 2011 16:03:05 +0100] rev 45780
avoid multiple TFF1 declarations
blanchet [Wed, 07 Dec 2011 16:03:05 +0100] rev 45779
updated TFF1 support
blanchet [Wed, 07 Dec 2011 16:03:05 +0100] rev 45778
updated Metis to 20110926 version
hoelzl [Wed, 07 Dec 2011 15:10:29 +0100] rev 45777
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
huffman [Mon, 05 Dec 2011 15:10:15 +0100] rev 45776
remove mem_(c)ball_0 and centre_in_(c)ball from simpset, as rules mem_(c)ball always match instead
huffman [Wed, 07 Dec 2011 10:50:30 +0100] rev 45775
add cancellation simprocs for type enat
nipkow [Wed, 07 Dec 2011 11:24:45 +0100] rev 45774
tuned
bulwahn [Tue, 06 Dec 2011 15:23:16 +0100] rev 45773
increasing quickcheck's timeout in the example theory to avoid failures on the testing infrastructure
hoelzl [Tue, 06 Dec 2011 14:29:37 +0100] rev 45772
tuned proofs
nipkow [Tue, 06 Dec 2011 14:18:24 +0100] rev 45771
added lemmas
nipkow [Mon, 05 Dec 2011 22:29:43 +0100] rev 45770
tuned proof
hoelzl [Mon, 05 Dec 2011 17:33:57 +0100] rev 45769
real is better supported than real_of_nat, use it in the nat => ereal coercion