| Wed, 25 Sep 2013 16:43:46 +0200 |
blanchet |
filled in gap in library offering
|
file |
diff |
annotate
|
| Wed, 25 Sep 2013 14:28:10 +0200 |
blanchet |
break more conjunctions
|
file |
diff |
annotate
|
| Wed, 18 Sep 2013 20:43:55 +0200 |
blanchet |
enrich data structure
|
file |
diff |
annotate
|
| Thu, 29 Aug 2013 15:02:42 +0200 |
blanchet |
rationalized bindings
|
file |
diff |
annotate
|
| Fri, 16 Aug 2013 19:03:31 +0200 |
blanchet |
renamed function
|
file |
diff |
annotate
|
| Fri, 16 Aug 2013 18:56:33 +0200 |
blanchet |
eliminate quasi-duplicate function
|
file |
diff |
annotate
|
| Fri, 16 Aug 2013 18:45:57 +0200 |
blanchet |
generalized "mk_permute"
|
file |
diff |
annotate
|
| Fri, 16 Aug 2013 18:36:55 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Fri, 16 Aug 2013 18:14:58 +0200 |
blanchet |
added more functions to BNF library
|
file |
diff |
annotate
|
| Fri, 16 Aug 2013 18:06:37 +0200 |
blanchet |
moved function to where it seems to belong
|
file |
diff |
annotate
|
| Fri, 16 Aug 2013 18:04:39 +0200 |
blanchet |
moved library function where it belongs, and used Dmitriy's inside-out implementation
|
file |
diff |
annotate
|
| Mon, 12 Aug 2013 15:36:55 +0200 |
traytel |
generalized library function
|
file |
diff |
annotate
|
| Mon, 12 Aug 2013 09:08:42 +0200 |
blanchet |
reverted ill-advised naming scheme of 5a77edcdbe54
|
file |
diff |
annotate
|
| Sun, 11 Aug 2013 23:35:59 +0200 |
blanchet |
made code more robust
|
file |
diff |
annotate
|
| Fri, 09 Aug 2013 15:03:39 +0200 |
blanchet |
honor user type names if possible
|
file |
diff |
annotate
|
| Thu, 08 Aug 2013 16:38:28 +0200 |
traytel |
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
|
file |
diff |
annotate
|
| Mon, 22 Jul 2013 21:12:15 +0200 |
traytel |
transfer rule for map (not yet registered as a transfer rule)
|
file |
diff |
annotate
|
| Sun, 07 Jul 2013 10:24:00 +0200 |
traytel |
Func -> Func_option, Ffunc -> Func (avoids dependence of codatatypes on the option type)
|
file |
diff |
annotate
|
| Fri, 31 May 2013 14:08:48 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Fri, 31 May 2013 12:28:39 +0200 |
blanchet |
renamed util function
|
file |
diff |
annotate
|
| Mon, 20 May 2013 13:29:45 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 07 May 2013 16:15:21 +0200 |
blanchet |
move function to library
|
file |
diff |
annotate
|
| Tue, 07 May 2013 14:47:22 +0200 |
traytel |
tuned
|
file |
diff |
annotate
|
| Tue, 07 May 2013 14:22:54 +0200 |
traytel |
got rid of the set based relator---use (binary) predicate based relator instead
|
file |
diff |
annotate
|
| Thu, 02 May 2013 15:08:59 +0200 |
blanchet |
one more lib function
|
file |
diff |
annotate
|
| Fri, 26 Apr 2013 12:09:51 +0200 |
blanchet |
more intuitive syntax for equality-style discriminators of nullary constructors
|
file |
diff |
annotate
|
| Fri, 26 Apr 2013 11:04:45 +0200 |
blanchet |
changed discriminator default: avoid mixing ctor and dtor views
|
file |
diff |
annotate
|
| Wed, 24 Apr 2013 18:49:52 +0200 |
blanchet |
honor user-specified name for relator + generalize syntax
|
file |
diff |
annotate
|
| Wed, 24 Apr 2013 15:42:00 +0200 |
blanchet |
derive "map_cong"
|
file |
diff |
annotate
|
| Wed, 24 Apr 2013 14:14:36 +0200 |
blanchet |
killed dead code
|
file |
diff |
annotate
|
| Wed, 24 Apr 2013 13:16:21 +0200 |
blanchet |
honor user-specified name for map function
|
file |
diff |
annotate
|
| Wed, 24 Apr 2013 13:16:20 +0200 |
blanchet |
honor user-specified set function names
|
file |
diff |
annotate
|
| Fri, 12 Oct 2012 21:22:35 +0200 |
wenzelm |
discontinued typedef with alternative name;
|
file |
diff |
annotate
|
| Fri, 12 Oct 2012 15:08:29 +0200 |
wenzelm |
discontinued typedef with implicit set_def;
|
file |
diff |
annotate
|
| Sun, 30 Sep 2012 22:02:34 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Thu, 27 Sep 2012 10:59:10 +0200 |
blanchet |
avoid another brand of trivial "disc_rel" theorems (which made the simplifier loop for all single-constructor types)
|
file |
diff |
annotate
|
| Wed, 26 Sep 2012 10:00:59 +0200 |
blanchet |
generate high-level "maps", "sets", and "rels" properties
|
file |
diff |
annotate
|
| Sun, 23 Sep 2012 14:52:53 +0200 |
blanchet |
started work on generation of "rel" theorems
|
file |
diff |
annotate
|
| Fri, 21 Sep 2012 16:45:06 +0200 |
blanchet |
renamed "Codatatype" directory "BNF" (and corresponding session) -- this opens the door to no-nonsense session names like "HOL-BNF-LFP"
|
file |
diff |
annotate
| base
|