Tue, 01 Oct 2013 14:05:25 +0200 |
blanchet |
renamed theory file
|
file |
diff |
annotate
|
Thu, 26 Sep 2013 16:25:12 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
Thu, 26 Sep 2013 16:17:34 +0200 |
blanchet |
avoid calls to nth with ~1
|
file |
diff |
annotate
|
Thu, 26 Sep 2013 13:56:07 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
Thu, 26 Sep 2013 13:42:14 +0200 |
blanchet |
generate "sel_splits(_asm)" theorems
|
file |
diff |
annotate
|
Thu, 26 Sep 2013 13:42:13 +0200 |
blanchet |
generate "sel_exhaust" theorem
|
file |
diff |
annotate
|
Thu, 26 Sep 2013 10:20:23 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
Thu, 26 Sep 2013 09:58:36 +0200 |
blanchet |
added data query function
|
file |
diff |
annotate
|
Wed, 25 Sep 2013 16:43:46 +0200 |
blanchet |
improved massaging of case expressions
|
file |
diff |
annotate
|
Wed, 25 Sep 2013 12:00:22 +0200 |
blanchet |
properly fold over branches
|
file |
diff |
annotate
|
Wed, 25 Sep 2013 10:45:12 +0200 |
blanchet |
keep a database of free constructor type information
|
file |
diff |
annotate
|
Wed, 25 Sep 2013 09:35:37 +0200 |
blanchet |
use case rather than sequence of ifs in expansion
|
file |
diff |
annotate
|
Tue, 24 Sep 2013 23:10:16 +0200 |
blanchet |
renamed generated property
|
file |
diff |
annotate
|
Tue, 24 Sep 2013 20:52:42 +0200 |
blanchet |
added [dest] to "disc_exclude"
|
file |
diff |
annotate
|
Tue, 24 Sep 2013 00:10:59 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
Tue, 24 Sep 2013 00:01:10 +0200 |
blanchet |
register codatatypes with Nitpick
|
file |
diff |
annotate
|
Mon, 23 Sep 2013 17:43:23 +0200 |
blanchet |
added [code] to selectors
|
file |
diff |
annotate
|
Mon, 23 Sep 2013 12:40:34 +0200 |
blanchet |
set [code] on case equations
|
file |
diff |
annotate
|
Thu, 19 Sep 2013 20:03:41 +0200 |
blanchet |
cleaner handling of collapse theorems
|
file |
diff |
annotate
|
Wed, 18 Sep 2013 19:57:59 +0200 |
blanchet |
include more "discI" rules
|
file |
diff |
annotate
|
Wed, 18 Sep 2013 18:53:24 +0200 |
blanchet |
note "discI"
|
file |
diff |
annotate
|
Wed, 18 Sep 2013 15:56:15 +0200 |
blanchet |
use singular to avoid confusion
|
file |
diff |
annotate
|
Mon, 09 Sep 2013 13:47:58 +0200 |
blanchet |
enriched data structure with necessary theorems
|
file |
diff |
annotate
|
Thu, 29 Aug 2013 18:24:11 +0200 |
blanchet |
handle type class annotations on (co)datatype parameters gracefully
|
file |
diff |
annotate
|
Mon, 26 Aug 2013 18:08:54 +0200 |
blanchet |
simplify code (now that ctr_sugar uses the same type variables as fp_sugar)
|
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
|
Mon, 12 Aug 2013 21:30:36 +0200 |
blanchet |
avoid double qualification for case constants
|
file |
diff |
annotate
|
Mon, 12 Aug 2013 15:25:17 +0200 |
blanchet |
clarified option name (since case/fold/rec are also destructors)
|
file |
diff |
annotate
|
Mon, 12 Aug 2013 15:25:17 +0200 |
blanchet |
define case constant from other 'free constructor' axioms
|
file |
diff |
annotate
|
Mon, 12 Aug 2013 09:51:00 +0200 |
blanchet |
handle both TVars and TFrees -- necessary for 'wrap_free_constructors'
|
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, 01 Aug 2013 14:22:21 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
Thu, 13 Jun 2013 17:26:39 -0400 |
blanchet |
store more theorems in data structure
|
file |
diff |
annotate
|
Thu, 06 Jun 2013 15:56:17 +0200 |
blanchet |
too much qualification is like too little
|
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
|
Thu, 02 May 2013 15:08:59 +0200 |
blanchet |
one more lib function
|
file |
diff |
annotate
|
Tue, 30 Apr 2013 16:04:50 +0200 |
blanchet |
renamed records
|
file |
diff |
annotate
|
Tue, 30 Apr 2013 15:58:32 +0200 |
blanchet |
added constructors to data structure
|
file |
diff |
annotate
|
Mon, 29 Apr 2013 17:37:00 +0200 |
blanchet |
create data structure for storing (co)datatype information
|
file |
diff |
annotate
|
Mon, 29 Apr 2013 16:50:01 +0200 |
blanchet |
use record instead of big tuple
|
file |
diff |
annotate
|
Mon, 29 Apr 2013 11:04:56 +0200 |
blanchet |
code tuning
|
file |
diff |
annotate
|
Sat, 27 Apr 2013 20:50:20 +0200 |
wenzelm |
uniform Proof.context for hyp_subst_tac;
|
file |
diff |
annotate
|
Sat, 27 Apr 2013 11:37:50 +0200 |
blanchet |
tuned ML and thy file names
|
file |
diff |
annotate
| base
|