| 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
|