| Wed, 04 Mar 2015 19:53:18 +0100 |
wenzelm |
tuned signature -- prefer qualified names;
|
file |
diff |
annotate
|
| Tue, 03 Mar 2015 19:08:04 +0100 |
traytel |
eliminated some clones of Proof_Context.cterm_of
|
file |
diff |
annotate
|
| Wed, 26 Nov 2014 20:05:34 +0100 |
wenzelm |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
file |
diff |
annotate
|
| Mon, 10 Nov 2014 21:49:48 +0100 |
wenzelm |
proper context for assume_tac (atac remains as fall-back without context);
|
file |
diff |
annotate
|
| Mon, 13 Oct 2014 18:45:48 +0200 |
wenzelm |
Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
|
file |
diff |
annotate
|
| Wed, 08 Oct 2014 17:09:07 +0200 |
wenzelm |
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
|
file |
diff |
annotate
|
| Mon, 08 Sep 2014 23:09:25 +0200 |
blanchet |
made 'lifting' plugin more robust
|
file |
diff |
annotate
|
| Fri, 05 Sep 2014 00:41:01 +0200 |
blanchet |
pretend code generation is a ctr_sugar plugin
|
file |
diff |
annotate
|
| Fri, 05 Sep 2014 00:41:01 +0200 |
blanchet |
named interpretations
|
file |
diff |
annotate
|
| Thu, 04 Sep 2014 09:02:43 +0200 |
blanchet |
tuned size function generation
|
file |
diff |
annotate
|
| Wed, 03 Sep 2014 22:49:05 +0200 |
blanchet |
introduced local interpretation mechanism for BNFs, to solve issues with datatypes in locales
|
file |
diff |
annotate
|
| Mon, 11 Aug 2014 10:43:03 +0200 |
traytel |
use Goal.prove_sorry instead of Goal.prove where possible (= no schematics in goal and tactic is expected to succeed)
|
file |
diff |
annotate
|
| Wed, 23 Apr 2014 17:57:56 +0200 |
kuncar |
predicator simplification rules: support also partially specialized types e.g. 'a * nat
|
file |
diff |
annotate
|
| Thu, 10 Apr 2014 17:48:18 +0200 |
kuncar |
setup for Transfer and Lifting from BNF; tuned thm names
|
file |
diff |
annotate
|