nipkow [Tue, 13 Dec 2011 16:53:28 +0100] rev 45834
connect while_option with lfp
nipkow [Tue, 13 Dec 2011 16:14:41 +0100] rev 45833
lemmas about Kleene iteration
wenzelm [Tue, 13 Dec 2011 15:19:30 +0100] rev 45832
merged
blanchet [Tue, 13 Dec 2011 14:55:42 +0100] rev 45831
avoid multiple type decls in TFF (improves on cef82dc1462d)
blanchet [Tue, 13 Dec 2011 14:55:42 +0100] rev 45830
added missing quantifier
blanchet [Tue, 13 Dec 2011 14:55:42 +0100] rev 45829
remove needless declaration in TFF1 problems
blanchet [Tue, 13 Dec 2011 14:55:42 +0100] rev 45828
correctly declare implicit TFF1 types that appear first as type arguments with "$tType" and not "$i
wenzelm [Tue, 13 Dec 2011 15:18:52 +0100] rev 45827
modernized specifications;
kuncar [Tue, 13 Dec 2011 14:04:20 +0100] rev 45826
support phantom types as quotient types
wenzelm [Mon, 12 Dec 2011 23:06:41 +0100] rev 45825
merged
nipkow [Mon, 12 Dec 2011 20:28:34 +0100] rev 45824
merged
nipkow [Mon, 12 Dec 2011 20:28:19 +0100] rev 45823
tuned
wenzelm [Mon, 12 Dec 2011 23:05:21 +0100] rev 45822
datatype dtyp with explicit sort information;
tuned messages;
wenzelm [Mon, 12 Dec 2011 20:55:57 +0100] rev 45821
tuned;
wenzelm [Mon, 12 Dec 2011 19:47:50 +0100] rev 45820
updated generated file;
bulwahn [Mon, 12 Dec 2011 17:22:48 +0100] rev 45819
tuned quickcheck's response
bulwahn [Mon, 12 Dec 2011 13:45:54 +0100] rev 45818
hiding constants and facts in the Quickcheck_Exhaustive and Quickcheck_Narrowing theory;
huffman [Mon, 12 Dec 2011 12:03:34 +0100] rev 45817
merged
huffman [Mon, 12 Dec 2011 08:19:37 +0100] rev 45816
replace more uses of 'lemmas' with explicit 'lemma';
replace uses of 'simplified' attribute with 'unfolded';
remove unused intermediate lemmas.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 12 Dec 2011 15:32:54 +0900] rev 45815
Add Quotient_Rat: an example of using the quotient package with partial equivalence relations, defining rational numbers.
huffman [Sun, 11 Dec 2011 21:57:22 +0100] rev 45814
fix spelling
huffman [Sun, 11 Dec 2011 21:54:20 +0100] rev 45813
fix spelling
nipkow [Sun, 11 Dec 2011 18:22:06 +0100] rev 45812
added IMP/Live_True.thy
huffman [Sun, 11 Dec 2011 09:55:57 +0100] rev 45811
replace many uses of 'lemmas' with 'lemma';
remove many unused intermediate lemmas.
huffman [Sat, 10 Dec 2011 22:00:42 +0100] rev 45810
prove class instances without extra lemmas
huffman [Sat, 10 Dec 2011 21:48:16 +0100] rev 45809
finite class instance for word type; remove unused lemmas
huffman [Sat, 10 Dec 2011 21:07:59 +0100] rev 45808
remove unused lemmas
huffman [Sat, 10 Dec 2011 16:24:22 +0100] rev 45807
generalize some lemmas
huffman [Sat, 10 Dec 2011 13:00:58 +0100] rev 45806
merged
huffman [Sat, 10 Dec 2011 08:29:19 +0100] rev 45805
tidied Word.thy;
put attributes directly on lemmas instead of using 'declare';
replace various 'lemmas' commands with ordinary 'lemma'.
huffman [Fri, 09 Dec 2011 14:52:51 +0100] rev 45804
remove redundant lemma word_diff_minus
huffman [Fri, 09 Dec 2011 14:14:05 +0100] rev 45803
remove some duplicate lemmas, simplify some proofs
kuncar [Fri, 09 Dec 2011 18:07:04 +0100] rev 45802
Quotient_Info stores only relation maps
bulwahn [Fri, 09 Dec 2011 16:08:32 +0100] rev 45801
hiding definitional facts in Quickcheck; introducing catch_match more honestly
kuncar [Fri, 09 Dec 2011 14:46:18 +0100] rev 45800
added dependencies
kuncar [Fri, 09 Dec 2011 14:22:05 +0100] rev 45799
added an example file with lifting of constants with contravariant and co/contravariant types
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