| 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
|
| Thu, 25 Apr 2013 18:27:26 +0200 |
blanchet |
renamed "wrap_data" to "wrap_free_constructors"
|
file |
diff |
annotate
|
| Thu, 25 Apr 2013 17:13:24 +0200 |
blanchet |
generate proper attributes for coinduction rules
|
file |
diff |
annotate
|
| Thu, 25 Apr 2013 09:25:50 +0200 |
blanchet |
start making "wrap_data" more robust
|
file |
diff |
annotate
|
| Thu, 25 Apr 2013 08:56:37 +0200 |
blanchet |
no eta-expansion for case in split rules and case_conv
|
file |
diff |
annotate
|
| Wed, 24 Apr 2013 16:21:23 +0200 |
blanchet |
apply arguments to f and g in "case_cong"
|
file |
diff |
annotate
|
| Wed, 24 Apr 2013 14:05:16 +0200 |
blanchet |
eta-contracted weak congruence rules (like in the old package)
|
file |
diff |
annotate
|
| Wed, 24 Apr 2013 13:16:20 +0200 |
blanchet |
honor user-specified set function names
|
file |
diff |
annotate
|
| Tue, 23 Apr 2013 16:49:14 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Tue, 23 Apr 2013 16:41:59 +0200 |
blanchet |
fix bugs in expand tactic w.r.t. datatypes with "needless" discriminators (e.g. lists with is_Nil instead of ~= Nil)
|
file |
diff |
annotate
|
| Thu, 18 Apr 2013 17:07:01 +0200 |
wenzelm |
simplifier uses proper Proof.context instead of historic type simpset;
|
file |
diff |
annotate
|
| Thu, 11 Apr 2013 16:58:54 +0200 |
traytel |
do not add case translation syntax in rep_datatype compatibility mode
|
file |
diff |
annotate
|
| Thu, 11 Apr 2013 16:39:01 +0200 |
traytel |
run type inference on input to wrap_data
|
file |
diff |
annotate
|
| Thu, 11 Apr 2013 16:03:11 +0200 |
traytel |
installed case translations in BNF package
|
file |
diff |
annotate
|
| Wed, 27 Mar 2013 14:19:18 +0100 |
wenzelm |
tuned signature and module arrangement;
|
file |
diff |
annotate
|
| Fri, 08 Mar 2013 14:15:39 +0100 |
blanchet |
proper type inference for default values
|
file |
diff |
annotate
|
| Mon, 26 Nov 2012 14:43:28 +0100 |
wenzelm |
tuned command descriptions;
|
file |
diff |
annotate
|
| Wed, 03 Oct 2012 21:46:52 +0200 |
blanchet |
made code more conform to rest of BNF package
|
file |
diff |
annotate
|
| Sun, 30 Sep 2012 22:02:34 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Sun, 30 Sep 2012 12:08:16 +0200 |
traytel |
use Thm.close_derivation in theorems proved using Skip_Proof.prove; tuned signature;
|
file |
diff |
annotate
|
| Fri, 28 Sep 2012 09:12:50 +0200 |
blanchet |
compatibility option to use "rep_datatype"
|
file |
diff |
annotate
|
| Thu, 27 Sep 2012 18:39:17 +0200 |
blanchet |
use a nicer scheme to indexify names
|
file |
diff |
annotate
|
| Thu, 27 Sep 2012 17:54:35 +0200 |
blanchet |
repaired signature
|
file |
diff |
annotate
|
| Thu, 27 Sep 2012 17:00:54 +0200 |
blanchet |
lower the defaults for the number of bits, based on an example by Lukas Bulwahn
|
file |
diff |
annotate
|
| Wed, 26 Sep 2012 10:01:00 +0200 |
blanchet |
tweaked theorem names (in particular, dropped s's)
|
file |
diff |
annotate
|
| Wed, 26 Sep 2012 10:00:59 +0200 |
blanchet |
generate high-level "coinduct" and "strong_coinduct" properties
|
file |
diff |
annotate
|
| Wed, 26 Sep 2012 10:00:59 +0200 |
blanchet |
parameterized "subst_tac"
|
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
|