| Sun, 26 Nov 2017 21:08:32 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Tue, 11 Jul 2017 21:36:42 +0200 |
traytel |
store the unfolded definitions of the lifted bnf constants under "_def" name
|
file |
diff |
annotate
|
| Tue, 19 Apr 2016 13:05:50 +0200 |
traytel |
unfold internal definitions before emitting a proof obligation
|
file |
diff |
annotate
|
| Wed, 13 Apr 2016 18:01:05 +0200 |
wenzelm |
eliminated "xname" and variants;
|
file |
diff |
annotate
|
| Thu, 31 Mar 2016 08:38:50 +0200 |
traytel |
tuned interface
|
file |
diff |
annotate
|
| Tue, 22 Mar 2016 08:00:33 +0100 |
blanchet |
nicer error
|
file |
diff |
annotate
|
| Mon, 14 Mar 2016 21:37:49 +0100 |
blanchet |
generalized ML function
|
file |
diff |
annotate
|
| Tue, 16 Feb 2016 22:28:19 +0100 |
traytel |
make predicator a first-class bnf citizen
|
file |
diff |
annotate
|
| Tue, 12 Jan 2016 09:28:08 +0100 |
traytel |
more careful witness' type analysis
|
file |
diff |
annotate
|
| Sun, 13 Dec 2015 21:56:15 +0100 |
wenzelm |
more general types Proof.method / context_tactic;
|
file |
diff |
annotate
|
| Mon, 31 Aug 2015 22:44:07 +0200 |
wenzelm |
misc tuning and simplification;
|
file |
diff |
annotate
|
| Mon, 31 Aug 2015 22:30:41 +0200 |
wenzelm |
proper option, not catch-all pattern;
|
file |
diff |
annotate
|
| Mon, 31 Aug 2015 20:55:22 +0200 |
wenzelm |
misc tuning and clarification;
|
file |
diff |
annotate
|
| Thu, 13 Aug 2015 16:47:00 +0200 |
traytel |
unfold intermediate definitions (stemming from composition) in lifted bnf operations
|
file |
diff |
annotate
|
| Wed, 12 Aug 2015 20:46:33 +0200 |
traytel |
new command for lifting BNF structure over typedefs
|
file |
diff |
annotate
|