| Mon, 27 Jul 2015 11:30:10 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 27 Jul 2015 00:17:18 +0200 |
wenzelm |
added infer_instantiate_vars, which allows inconsistent types for variables, as required for Metis proof reconstruction;
|
file |
diff |
annotate
|
| Sun, 26 Jul 2015 20:54:02 +0200 |
wenzelm |
ignore non-existant variables, like other instantiate rules;
|
file |
diff |
annotate
|
| Sun, 26 Jul 2015 12:24:16 +0200 |
wenzelm |
added infer_instantiate';
|
file |
diff |
annotate
|
| Sun, 26 Jul 2015 11:08:57 +0200 |
wenzelm |
more uniform exceptions, like cterm_instantiate;
|
file |
diff |
annotate
|
| Sat, 25 Jul 2015 23:15:37 +0200 |
wenzelm |
more accurate maxidx;
|
file |
diff |
annotate
|
| Sat, 25 Jul 2015 21:54:09 +0200 |
wenzelm |
clarified error;
|
file |
diff |
annotate
|
| Sat, 25 Jul 2015 21:37:09 +0200 |
wenzelm |
added infer_instantiate, which is meant to supersede cterm_instantiate;
|
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
|
| Wed, 03 Jun 2015 19:25:05 +0200 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Sun, 31 May 2015 00:20:35 +0200 |
wenzelm |
obsolete;
|
file |
diff |
annotate
|
| Sun, 31 May 2015 00:11:12 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 30 May 2015 23:58:06 +0200 |
wenzelm |
standardize towards Thm.eta_long_conversion, which just does eta_long conversion;
|
file |
diff |
annotate
|
| Sat, 30 May 2015 22:04:15 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 30 May 2015 21:52:37 +0200 |
wenzelm |
more explicit context;
|
file |
diff |
annotate
|
| Sat, 30 May 2015 21:28:01 +0200 |
wenzelm |
obsolete;
|
file |
diff |
annotate
|
| Sat, 30 May 2015 20:21:53 +0200 |
wenzelm |
tuned -- more direct Thm.renamed_prop;
|
file |
diff |
annotate
|
| Sun, 03 May 2015 16:44:38 +0200 |
wenzelm |
suppress formal sort-constraints, in accordance to norm_hhf_eqs;
|
file |
diff |
annotate
|
| Fri, 10 Apr 2015 11:29:12 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 31 Mar 2015 00:11:54 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 22 Mar 2015 12:38:41 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 20 Mar 2015 11:09:08 +0100 |
wenzelm |
tuned -- prepare instantiation more uniformly;
|
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
|
| Thu, 05 Mar 2015 13:28:04 +0100 |
wenzelm |
tuned -- more explicit use of context;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 23:21:09 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 22:05:01 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 19:53:18 +0100 |
wenzelm |
tuned signature -- prefer qualified names;
|
file |
diff |
annotate
|
| Wed, 26 Nov 2014 20:05:34 +0100 |
wenzelm |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
file |
diff |
annotate
|
| Sat, 08 Nov 2014 21:31:51 +0100 |
wenzelm |
optional proof context for unify operations, for the sake of proper local options;
|
file |
diff |
annotate
|
| Sun, 06 Apr 2014 15:43:45 +0200 |
wenzelm |
more source positions;
|
file |
diff |
annotate
|
| Fri, 21 Mar 2014 20:33:56 +0100 |
wenzelm |
more qualified names;
|
file |
diff |
annotate
|
| Thu, 27 Jun 2013 17:06:22 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 27 Jun 2013 11:33:42 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 29 May 2013 18:52:35 +0200 |
wenzelm |
more precise "incremented" indication, which might be relevant in corner cases, e.g. instantiation of leading to vars with different types (which is a potential problem nonetheless);
|
file |
diff |
annotate
|
| Wed, 29 May 2013 18:25:11 +0200 |
wenzelm |
tuned signature -- more explicit flags for low-level Thm.bicompose;
|
file |
diff |
annotate
|
| Fri, 24 May 2013 17:00:46 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 25 Jun 2012 17:50:05 +0200 |
wenzelm |
eliminated obsolete swap_prems_rl -- rotate_prems usually does the job more directly;
|
file |
diff |
annotate
|
| Wed, 11 Apr 2012 21:40:46 +0200 |
wenzelm |
rule composition via attribute "OF" (or ML functions OF/MRS) is more tolerant against multiple unifiers;
|
file |
diff |
annotate
|
| Sat, 31 Mar 2012 19:26:23 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 19 Mar 2012 21:10:33 +0100 |
wenzelm |
moved some legacy stuff;
|
file |
diff |
annotate
|
| Wed, 15 Feb 2012 23:19:30 +0100 |
wenzelm |
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
|
file |
diff |
annotate
|
| Wed, 15 Feb 2012 22:44:31 +0100 |
wenzelm |
discontinued Drule.term_rule, which tends to cause confusion due to builtin cterm_of (NB: the standard morphisms already provide a separate term component);
|
file |
diff |
annotate
|
| Tue, 14 Feb 2012 20:57:05 +0100 |
wenzelm |
discontinued unused MRL -- in correspondence with section "2.4.2 Rule composition" in the implementation manual;
|
file |
diff |
annotate
|
| Sat, 14 Jan 2012 16:58:29 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 11 Jan 2012 16:25:34 +0100 |
wenzelm |
more qualified names;
|
file |
diff |
annotate
|
| Sat, 05 Nov 2011 20:32:12 +0100 |
wenzelm |
tuned cterm_instantiate: avoid somewhat expensive Term.map_types and cterm_of;
|
file |
diff |
annotate
|
| Sat, 05 Nov 2011 20:07:38 +0100 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
| Sun, 16 Oct 2011 18:48:30 +0200 |
wenzelm |
added Term.dummy_pattern conveniences;
|
file |
diff |
annotate
|
| Wed, 10 Aug 2011 19:45:41 +0200 |
wenzelm |
avoid OldTerm operations -- with subtle changes of semantics;
|
file |
diff |
annotate
|
| Mon, 27 Jun 2011 15:03:55 +0200 |
wenzelm |
old gensym is now legacy -- global state is out of fashion, and its result is not guaranteed to be fresh;
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 23:12:02 +0200 |
wenzelm |
renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 20:56:08 +0200 |
wenzelm |
clarified special incr_type_indexes;
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 16:34:49 +0200 |
wenzelm |
discontinued Name.variant to emphasize that this is old-style / indirect;
|
file |
diff |
annotate
|
| Sat, 23 Apr 2011 19:41:53 +0200 |
wenzelm |
hardwired mapping "_" -> "Pure.asm_rl" avoids legacy binding;
|
file |
diff |
annotate
|
| Fri, 26 Nov 2010 22:29:41 +0100 |
wenzelm |
make two copies (!) of Library.UnequalLengths coincide with ListPair.UnequalLengths;
|
file |
diff |
annotate
|
| Mon, 20 Sep 2010 16:05:25 +0200 |
wenzelm |
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
|
file |
diff |
annotate
|
| Wed, 25 Aug 2010 15:12:49 +0200 |
wenzelm |
structure Thm: less pervasive names;
|
file |
diff |
annotate
|
| Sat, 15 May 2010 21:41:32 +0200 |
wenzelm |
less pervasive names from structure Thm;
|
file |
diff |
annotate
|
| Mon, 03 May 2010 20:13:36 +0200 |
wenzelm |
renamed Thm.freezeT to Thm.legacy_freezeT -- it is based on Type.legacy_freeze;
|
file |
diff |
annotate
|