| Mon, 20 Jan 2014 23:07:23 +0100 |
blanchet |
moved 'bacc' back to 'Enum' (cf. 744934b818c7) -- reduces baggage loaded by 'Hilbert_Choice'
|
file |
diff |
annotate
|
| Wed, 01 Jan 2014 01:05:48 +0100 |
haftmann |
fundamental treatment of undefined vs. universally partial replaces code_abort
|
file |
diff |
annotate
|
| Sun, 10 Nov 2013 15:05:06 +0100 |
haftmann |
qualifed popular user space names
|
file |
diff |
annotate
|
| Fri, 18 Oct 2013 10:43:21 +0200 |
blanchet |
killed more "no_atp"s
|
file |
diff |
annotate
|
| Tue, 13 Aug 2013 16:25:47 +0200 |
wenzelm |
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
|
file |
diff |
annotate
|
| Sun, 23 Jun 2013 21:16:07 +0200 |
haftmann |
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
|
file |
diff |
annotate
|
| Sun, 16 Dec 2012 18:07:29 +0100 |
bulwahn |
providing a custom code equation for vimage to overwrite the vimage definition that would be rewritten by set_comprehension_pointfree simproc in the code preprocessor to an non-terminating code equation
|
file |
diff |
annotate
|
| Mon, 22 Oct 2012 22:24:34 +0200 |
haftmann |
incorporated constant chars into instantiation proof for enum;
|
file |
diff |
annotate
|
| Sat, 20 Oct 2012 10:00:21 +0200 |
haftmann |
tailored enum specification towards simple instantiation;
|
file |
diff |
annotate
|
| Sat, 20 Oct 2012 10:00:21 +0200 |
haftmann |
refined internal structure of Enum.thy
|
file |
diff |
annotate
|
| Sat, 20 Oct 2012 09:12:16 +0200 |
haftmann |
moved quite generic material from theory Enum to more appropriate places
|
file |
diff |
annotate
|
| 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
|