| Wed, 13 Apr 2016 18:01:05 +0200 |
wenzelm |
eliminated "xname" and variants;
|
file |
diff |
annotate
|
| Sat, 05 Mar 2016 12:49:47 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 13 Dec 2015 21:56:15 +0100 |
wenzelm |
more general types Proof.method / context_tactic;
|
file |
diff |
annotate
|
| Sat, 17 Oct 2015 22:31:21 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 26 Jul 2015 17:24:54 +0200 |
wenzelm |
updated to infer_instantiate;
|
file |
diff |
annotate
|
| Sat, 18 Jul 2015 20:47:08 +0200 |
wenzelm |
prefer tactics with explicit context;
|
file |
diff |
annotate
|
| Thu, 16 Jul 2015 12:23:22 +0200 |
traytel |
{r,e,d,f}tac with proper context in BNF
|
file |
diff |
annotate
|
| Mon, 06 Jul 2015 19:33:30 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 15 Jun 2015 15:33:38 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 07 Jun 2015 20:03:40 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 03 May 2015 14:35:48 +0200 |
wenzelm |
make SML/NJ more happy;
|
file |
diff |
annotate
|
| Sat, 02 May 2015 13:58:06 +0200 |
kuncar |
handle error messages also in after_qed
|
file |
diff |
annotate
|
| Sat, 02 May 2015 13:58:06 +0200 |
kuncar |
reorder some steps in the construction to support mutual datatypes
|
file |
diff |
annotate
|
| Sat, 02 May 2015 13:58:06 +0200 |
kuncar |
more readable error message if some types do not correspond to sort constraints of the datatype
|
file |
diff |
annotate
|
| Sat, 02 May 2015 13:58:06 +0200 |
kuncar |
better precomputing
|
file |
diff |
annotate
|
| Sat, 02 May 2015 13:58:06 +0200 |
kuncar |
equivalence in code_dt data structure must respect both rty and qty
|
file |
diff |
annotate
|
| Sat, 02 May 2015 13:58:06 +0200 |
kuncar |
don't use the human-readable version of the rsp thm as a goal in the ML interface (there is no formal definition of its statement); make tactics more robust wrt. predicates in predicators; tuned
|
file |
diff |
annotate
|
| Mon, 13 Apr 2015 15:27:34 +0200 |
kuncar |
go back to the complicated code equation registration (because of type classes) that was lost in 922586b1bc87; make it even more hackish to get which code equation was used
|
file |
diff |
annotate
|
| Fri, 05 Dec 2014 14:14:36 +0100 |
kuncar |
Workaround that allows us to execute lifted constants that have as a return type a datatype containing a subtype
|
file |
diff |
annotate
|