| 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
|