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