| Wed, 17 Feb 2016 11:54:34 +0100 |
blanchet |
allow predicator instead of map function in 'primrec'
|
file |
diff |
annotate
|
| Mon, 15 Feb 2016 18:27:17 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Mon, 15 Feb 2016 12:48:10 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Tue, 01 Dec 2015 13:07:40 +0100 |
blanchet |
tuned whitespace
|
file |
diff |
annotate
|
| Mon, 02 Nov 2015 21:49:49 +0100 |
blanchet |
allow selectors and discriminators with same name as type
|
file |
diff |
annotate
|
| Tue, 06 Oct 2015 12:01:07 +0200 |
traytel |
collect the names from goals in favor of fragile exports
|
file |
diff |
annotate
|
| Thu, 01 Oct 2015 17:32:07 +0200 |
blanchet |
export '_cmd' functions
|
file |
diff |
annotate
|
| Fri, 25 Sep 2015 23:01:34 +0200 |
traytel |
restructure fresh variable generation to make exports more wellformed
|
file |
diff |
annotate
|
| Fri, 25 Sep 2015 23:01:31 +0200 |
traytel |
more canonical context threading
|
file |
diff |
annotate
|
| Fri, 04 Sep 2015 21:40:59 +0200 |
wenzelm |
close derivation *before* splitting conjuncts, like Goal.prove_common (see also 757cad5a3fe9) -- potential improvement of performance;
|
file |
diff |
annotate
|
| Thu, 03 Sep 2015 16:41:43 +0200 |
traytel |
use open/close_target rather than Local_Theory.restore to get polymorphic definitions;
|
file |
diff |
annotate
|
| Tue, 28 Jul 2015 20:59:39 +0200 |
wenzelm |
more explicit context;
|
file |
diff |
annotate
|
| Mon, 27 Jul 2015 17:44:55 +0200 |
wenzelm |
tuned signature;
|
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
|
| Sun, 05 Jul 2015 15:02:30 +0200 |
wenzelm |
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
|
file |
diff |
annotate
|
| Sat, 09 May 2015 14:10:10 +0200 |
blanchet |
took out unreliable 'blast' from tactic altogether
|
file |
diff |
annotate
|
| Sun, 03 May 2015 18:14:11 +0200 |
blanchet |
made split-rule tactic go beyond constructors with 20 arguments
|
file |
diff |
annotate
|
| Mon, 06 Apr 2015 17:06:48 +0200 |
wenzelm |
@{command_spec} is superseded by @{command_keyword};
|
file |
diff |
annotate
|
| Tue, 31 Mar 2015 00:11:54 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 07 Mar 2015 21:32:31 +0100 |
wenzelm |
clarified Drule.gen_all: observe context more carefully;
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 15:58:56 +0100 |
wenzelm |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
file |
diff |
annotate
|
| 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
|
| Mon, 05 Jan 2015 21:24:14 +0100 |
blanchet |
generate [code] only with 'code' plugin enabled
|
file |
diff |
annotate
|
| Mon, 05 Jan 2015 10:09:42 +0100 |
blanchet |
added plugins syntax to prim(co)rec
|
file |
diff |
annotate
|
| Mon, 05 Jan 2015 06:56:15 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Fri, 19 Dec 2014 11:18:58 +0100 |
desharna |
generate 'disc_eq_case' for Ctr_Sugars
|
file |
diff |
annotate
|
| Mon, 05 Jan 2015 06:56:15 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Fri, 19 Dec 2014 11:17:23 +0100 |
desharna |
generate 'case_distrib' for Ctr_Sugars
|
file |
diff |
annotate
|
| Wed, 26 Nov 2014 20:05:34 +0100 |
wenzelm |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
file |
diff |
annotate
|
| Thu, 13 Nov 2014 17:28:11 +0100 |
blanchet |
tuning
|
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
|
| Wed, 15 Oct 2014 17:18:08 +0200 |
blanchet |
made SML/NJ happier
|
file |
diff |
annotate
|
| Tue, 14 Oct 2014 16:17:34 +0200 |
desharna |
add 'kind' to 'cr_sugar'
|
file |
diff |
annotate
|
| Mon, 13 Oct 2014 21:41:29 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 13 Oct 2014 19:34:10 +0200 |
wenzelm |
clarified load order;
|
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, 15 Sep 2014 10:49:07 +0200 |
blanchet |
generate 'code' attribute only if 'code' plugin is enabled
|
file |
diff |
annotate
|
| Thu, 11 Sep 2014 20:01:29 +0200 |
blanchet |
tuned comment
|
file |
diff |
annotate
|
| Tue, 09 Sep 2014 22:33:43 +0200 |
blanchet |
avoid exception
|
file |
diff |
annotate
|
| Tue, 09 Sep 2014 20:51:36 +0200 |
blanchet |
nicer case names in the N2M case, similar to those generated by the old package (e.g. 'Cons_tree' instead of just 'Cons')
|
file |
diff |
annotate
|
| Tue, 09 Sep 2014 20:51:36 +0200 |
blanchet |
generalized 'datatype' LaTeX antiquotation and added 'codatatype'
|
file |
diff |
annotate
|
| Mon, 08 Sep 2014 19:21:07 +0200 |
blanchet |
honour sorts in N2M
|
file |
diff |
annotate
|
| Mon, 08 Sep 2014 15:11:37 +0200 |
blanchet |
use right sort constraints
|
file |
diff |
annotate
|
| Mon, 08 Sep 2014 14:03:46 +0200 |
blanchet |
made SML/NJ happire
|
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 |
added 'plugins' option to control which hooks are enabled
|
file |
diff |
annotate
|
| Fri, 05 Sep 2014 00:41:01 +0200 |
blanchet |
introduced mechanism to filter interpretations
|
file |
diff |
annotate
|
| Fri, 05 Sep 2014 00:41:01 +0200 |
blanchet |
fixed infinite loops in 'register' functions + more uniform API
|
file |
diff |
annotate
|
| Fri, 05 Sep 2014 00:41:01 +0200 |
blanchet |
named interpretations
|
file |
diff |
annotate
|
| Fri, 05 Sep 2014 00:41:00 +0200 |
blanchet |
centralized and cleaned up naming handling
|
file |
diff |
annotate
|
| Thu, 04 Sep 2014 11:20:59 +0200 |
blanchet |
tweaked setup for datatype realizer
|
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
|
| Wed, 03 Sep 2014 22:47:48 +0200 |
blanchet |
tuned ctr_sugar database handling
|
file |
diff |
annotate
|
| Wed, 03 Sep 2014 00:06:23 +0200 |
blanchet |
take out 'x = C' of the simplifier for unit types
|
file |
diff |
annotate
|
| Mon, 01 Sep 2014 16:17:47 +0200 |
blanchet |
added theory-based getters for convenience
|
file |
diff |
annotate
|
| Mon, 01 Sep 2014 16:17:47 +0200 |
blanchet |
made transfer functions slightly more general
|
file |
diff |
annotate
|
| Mon, 18 Aug 2014 17:20:14 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Mon, 18 Aug 2014 17:20:13 +0200 |
blanchet |
added collection theorem for consistency and convenience
|
file |
diff |
annotate
|