| Mon, 25 Jun 2012 16:03:21 +0200 |
bulwahn |
some special code equations for Id with class constraint enum after adding the set comprehension simproc to the code preprocessing
|
file |
diff |
annotate
|
| Fri, 30 Mar 2012 17:25:34 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Fri, 30 Mar 2012 17:22:17 +0200 |
wenzelm |
tuned proofs, less guesswork;
|
file |
diff |
annotate
|
| Fri, 30 Mar 2012 14:00:18 +0200 |
huffman |
rephrase lemma card_Pow using '2' instead of 'Suc (Suc 0)'
|
file |
diff |
annotate
|
| Mon, 30 Jan 2012 13:55:24 +0100 |
bulwahn |
adding code equations for max_extp and mlex
|
file |
diff |
annotate
|
| Mon, 30 Jan 2012 13:55:22 +0100 |
bulwahn |
adding code equation for rtranclp in Enum
|
file |
diff |
annotate
|
| Mon, 30 Jan 2012 13:55:21 +0100 |
bulwahn |
adding code equation for max_ext
|
file |
diff |
annotate
|
| Mon, 30 Jan 2012 13:55:20 +0100 |
bulwahn |
adding code equation for tranclp
|
file |
diff |
annotate
|
| Sat, 28 Jan 2012 12:05:26 +0100 |
bulwahn |
an executable version of accessible part (only for finite types yet)
|
file |
diff |
annotate
|
| Thu, 26 Jan 2012 12:03:35 +0100 |
bulwahn |
evaluation of THE with a non-singleton set raises a Match exception during the evaluation to yield a potential counterexample in quickcheck.
|
file |
diff |
annotate
|
| Wed, 25 Jan 2012 09:32:23 +0100 |
bulwahn |
adding code equation for Collect on finite types
|
file |
diff |
annotate
|
| Sat, 24 Dec 2011 15:53:08 +0100 |
haftmann |
enum type class instance for `set`; dropped misfitting code lemma for trancl
|
file |
diff |
annotate
|
| Fri, 14 Oct 2011 18:55:59 +0200 |
haftmann |
moved sublists to More_List.thy
|
file |
diff |
annotate
|
| Thu, 13 Oct 2011 23:35:15 +0200 |
haftmann |
avoid very specific code equation for card; corrected spelling
|
file |
diff |
annotate
|
| Thu, 13 Oct 2011 23:27:46 +0200 |
haftmann |
bouned transitive closure
|
file |
diff |
annotate
|
| Mon, 03 Oct 2011 15:39:30 +0200 |
bulwahn |
tune text for document generation
|
file |
diff |
annotate
|
| Mon, 03 Oct 2011 14:43:14 +0200 |
bulwahn |
adding code equations for cardinality and (reflexive) transitive closure on finite types
|
file |
diff |
annotate
|
| Mon, 13 Dec 2010 08:51:52 +0100 |
bulwahn |
adding an executable THE operator on finite types
|
file |
diff |
annotate
|
| Wed, 08 Dec 2010 18:07:03 +0100 |
bulwahn |
adding a smarter enumeration scheme for finite functions
|
file |
diff |
annotate
|
| Wed, 08 Dec 2010 14:25:08 +0100 |
bulwahn |
adding more efficient implementations for quantifiers in Enum
|
file |
diff |
annotate
|
| Fri, 03 Dec 2010 08:40:46 +0100 |
bulwahn |
adding shorter output syntax for the finite types of quickcheck
|
file |
diff |
annotate
|
| Fri, 03 Dec 2010 08:40:46 +0100 |
bulwahn |
changed order of lemmas to overwrite the general code equation with the nbe-specific one
|
file |
diff |
annotate
|
| Wed, 24 Nov 2010 10:52:02 +0100 |
bulwahn |
removing Enum.in_enum from the claset
|
file |
diff |
annotate
|
| Mon, 22 Nov 2010 11:35:11 +0100 |
bulwahn |
hiding enum
|
file |
diff |
annotate
|
| Mon, 22 Nov 2010 11:35:07 +0100 |
bulwahn |
hiding the constants
|
file |
diff |
annotate
|
| Mon, 22 Nov 2010 11:34:58 +0100 |
bulwahn |
adding code equations for EX1 on finite types
|
file |
diff |
annotate
|
| Mon, 22 Nov 2010 11:34:57 +0100 |
bulwahn |
adding code equation for function equality; adding some instantiations for the finite types
|
file |
diff |
annotate
|
| Mon, 22 Nov 2010 11:34:56 +0100 |
bulwahn |
adding Enum to HOL-Main image and removing it from HOL-Library
|
file |
diff |
annotate
|
| Mon, 22 Nov 2010 11:34:55 +0100 |
bulwahn |
moving Enum theory from HOL/Library to HOL
|
file |
diff |
annotate
| base
|