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