| Wed, 22 Jan 2025 22:22:19 +0100 |
wenzelm |
misc tuning: more concise operations on prems (without change of exceptions);
|
file |
diff |
annotate
|
| Sun, 31 Dec 2023 22:39:40 +0100 |
wenzelm |
minor performance tuning: proper Same.operation;
|
file |
diff |
annotate
|
| Wed, 18 Oct 2023 15:13:52 +0200 |
wenzelm |
clarified signature: more concise variations on implicit theory setup;
|
file |
diff |
annotate
|
| Tue, 06 Jun 2023 11:33:38 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 15 May 2023 10:59:49 +0200 |
wenzelm |
tuned: more accurate check (is_norm_hhf protect);
|
file |
diff |
annotate
|
| Tue, 18 Apr 2023 22:24:48 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 10 Sep 2021 14:59:19 +0200 |
wenzelm |
clarified signature: more scalable operations;
|
file |
diff |
annotate
|
| Thu, 09 Sep 2021 17:20:41 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Thu, 09 Sep 2021 12:33:14 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Mon, 06 Sep 2021 14:05:22 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Mon, 06 Sep 2021 12:23:06 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Mon, 06 Sep 2021 12:11:17 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Mon, 06 Sep 2021 11:55:54 +0200 |
wenzelm |
more scalable operations;
|
file |
diff |
annotate
|
| Mon, 06 Sep 2021 11:32:18 +0200 |
wenzelm |
more efficient operations: traverse hyps only when required;
|
file |
diff |
annotate
|
| Sun, 05 Sep 2021 21:09:31 +0200 |
wenzelm |
more scalable operations;
|
file |
diff |
annotate
|
| Sun, 05 Sep 2021 19:47:06 +0200 |
wenzelm |
unused;
|
file |
diff |
annotate
|
| Sat, 04 Sep 2021 22:17:15 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 04 Sep 2021 22:05:35 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 04 Sep 2021 21:25:08 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 04 Sep 2021 18:21:58 +0200 |
wenzelm |
more scalable operations;
|
file |
diff |
annotate
|
| Fri, 03 Sep 2021 18:57:33 +0200 |
wenzelm |
more scalable data structure (but: rarely used many arguments);
|
file |
diff |
annotate
|
| Thu, 26 Aug 2021 14:45:19 +0200 |
wenzelm |
more scalable data structure (but: rarely used with > 5 arguments);
|
file |
diff |
annotate
|
| Fri, 09 Aug 2019 17:14:49 +0200 |
wenzelm |
formal position for PThm nodes;
|
file |
diff |
annotate
|
| Tue, 06 Aug 2019 16:29:28 +0200 |
wenzelm |
more robust and convenient treatment of implicit context;
|
file |
diff |
annotate
|
| Fri, 02 Aug 2019 11:23:09 +0200 |
wenzelm |
clarified modules: inference kernel maintains sort algebra within the logic;
|
file |
diff |
annotate
|
| Sat, 13 Apr 2019 21:43:41 +0200 |
wenzelm |
meson: more cterm operations;
|
file |
diff |
annotate
|
| Sat, 13 Apr 2019 16:42:19 +0200 |
wenzelm |
tuned signature -- more ctyp operations;
|
file |
diff |
annotate
|
| Mon, 01 Oct 2018 16:40:45 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 20 Sep 2018 22:39:39 +0200 |
wenzelm |
clarified standardization of variables, with proper treatment of local variables;
|
file |
diff |
annotate
|
| Mon, 06 Aug 2018 11:06:43 +0200 |
wenzelm |
export shyps as regular typargs;
|
file |
diff |
annotate
|
| Fri, 29 Jun 2018 14:19:52 +0200 |
wenzelm |
disallow hyps in export;
|
file |
diff |
annotate
|
| Sun, 25 Feb 2018 15:44:46 +0100 |
wenzelm |
eliminated ASCII syntax from Pure bootstrap;
|
file |
diff |
annotate
|
| Tue, 13 Dec 2016 11:51:42 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Thu, 28 Apr 2016 15:42:52 +0200 |
wenzelm |
unfold is subject to unfold_abs_def (still inactive);
|
file |
diff |
annotate
|
| Tue, 05 Apr 2016 20:03:24 +0200 |
wenzelm |
clarified modules -- simplified bootstrap;
|
file |
diff |
annotate
|
| Tue, 15 Dec 2015 16:57:10 +0100 |
wenzelm |
tuned signature -- clarified modules;
|
file |
diff |
annotate
|
| Sun, 16 Aug 2015 21:55:11 +0200 |
wenzelm |
produce certified vars without access to theory_of_thm, and without context;
|
file |
diff |
annotate
|
| Sun, 16 Aug 2015 19:25:08 +0200 |
wenzelm |
added Thm.chyps_of;
|
file |
diff |
annotate
|
| Tue, 28 Jul 2015 21:47:03 +0200 |
wenzelm |
more explicit context;
|
file |
diff |
annotate
|
| Tue, 28 Jul 2015 21:10:41 +0200 |
wenzelm |
clarified Variable.gen_all;
|
file |
diff |
annotate
|
| Tue, 28 Jul 2015 20:59:39 +0200 |
wenzelm |
more explicit context;
|
file |
diff |
annotate
|
| Tue, 28 Jul 2015 19:49:54 +0200 |
wenzelm |
more direct access to atomic cterms;
|
file |
diff |
annotate
|
| Mon, 27 Jul 2015 23:40:39 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 27 Jul 2015 17:44:55 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 27 Jul 2015 15:13:05 +0200 |
wenzelm |
more explicit checks -- improved errors;
|
file |
diff |
annotate
|
| Mon, 27 Jul 2015 14:56:06 +0200 |
wenzelm |
eliminated cterm_instantiate;
|
file |
diff |
annotate
|
| 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
|
| Sun, 25 Apr 2010 23:09:32 +0200 |
wenzelm |
renamed Drule.unconstrainTs to Thm.unconstrain_allTs to accomdate the version by krauss/schropp;
|
file |
diff |
annotate
|
| Sat, 27 Mar 2010 15:20:31 +0100 |
wenzelm |
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
|
file |
diff |
annotate
|
| Mon, 22 Mar 2010 19:29:11 +0100 |
wenzelm |
eliminated old-style Drule.add_axiom in favour of Specification.axiom, with explicit Drule.export_without_context to imitate the old behaviour;
|
file |
diff |
annotate
|
| Mon, 22 Mar 2010 00:48:56 +0100 |
wenzelm |
replaced PureThy.add_axioms by more basic Drule.add_axiom, which is old-style nonetheless;
|
file |
diff |
annotate
|
| Sat, 20 Mar 2010 17:33:11 +0100 |
wenzelm |
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
|
file |
diff |
annotate
|
| Fri, 19 Feb 2010 20:39:48 +0100 |
wenzelm |
moved ancient Drule.get_def to OldGoals.get_def;
|
file |
diff |
annotate
|
| Sun, 07 Feb 2010 19:33:34 +0100 |
wenzelm |
renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
|
file |
diff |
annotate
|
| Sat, 21 Nov 2009 15:49:29 +0100 |
wenzelm |
explicitly mark some legacy freeze operations;
|
file |
diff |
annotate
|
| Thu, 12 Nov 2009 22:02:11 +0100 |
wenzelm |
eliminated obsolete "internal" kind -- collapsed to unspecific "";
|
file |
diff |
annotate
|
| Mon, 02 Nov 2009 20:34:59 +0100 |
wenzelm |
modernized structure Simple_Syntax;
|
file |
diff |
annotate
|
| Wed, 28 Oct 2009 16:25:26 +0100 |
wenzelm |
Drule.store: proper binding;
|
file |
diff |
annotate
|
| Sat, 24 Oct 2009 19:47:37 +0200 |
wenzelm |
renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
|
file |
diff |
annotate
|
| Sat, 17 Oct 2009 00:53:18 +0200 |
wenzelm |
legacy Drule.standard is no longer pervasive;
|
file |
diff |
annotate
|
| Thu, 09 Jul 2009 22:48:12 +0200 |
wenzelm |
renamed structure TermSubst to Term_Subst;
|
file |
diff |
annotate
|
| Mon, 06 Jul 2009 21:24:30 +0200 |
wenzelm |
structure Thm: less pervasive names;
|
file |
diff |
annotate
|
| Thu, 02 Jul 2009 21:26:18 +0200 |
wenzelm |
renamed Drule.sort_triv to Thm.sort_triv (cf. more_thm.ML);
|
file |
diff |
annotate
|
| Mon, 16 Mar 2009 23:39:44 +0100 |
wenzelm |
refined is_norm_hhf: reject beta-redexes (rules based on term nets or could_unify assume normal form), also potentially faster by avoiding expensive Envir.beta_eta_contract;
|
file |
diff |
annotate
|
| Sat, 07 Mar 2009 22:04:59 +0100 |
wenzelm |
moved Thm.def_name(_optional) to more_thm.ML;
|
file |
diff |
annotate
|
| Wed, 21 Jan 2009 16:47:04 +0100 |
haftmann |
binding replaces bstring
|
file |
diff |
annotate
|
| Sun, 04 Jan 2009 15:28:09 +0100 |
wenzelm |
added comp_no_flatten;
|
file |
diff |
annotate
|
| Wed, 31 Dec 2008 18:53:16 +0100 |
wenzelm |
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
|
file |
diff |
annotate
|
| Wed, 31 Dec 2008 00:08:13 +0100 |
wenzelm |
moved old add_term_vars, add_term_frees etc. to structure OldTerm;
|
file |
diff |
annotate
|
| Fri, 31 Oct 2008 10:39:04 +0100 |
berghofe |
Theorem "_" is now stored with open derivation.
|
file |
diff |
annotate
|
| Thu, 23 Oct 2008 15:28:01 +0200 |
wenzelm |
renamed Thm.get_axiom_i to Thm.axiom;
|
file |
diff |
annotate
|
| Thu, 16 Oct 2008 22:44:27 +0200 |
wenzelm |
added rules for sort_constraint, include in norm_hhf_eqs;
|
file |
diff |
annotate
|
| Thu, 14 Aug 2008 16:52:46 +0200 |
wenzelm |
moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
|
file |
diff |
annotate
|
| Mon, 23 Jun 2008 23:45:46 +0200 |
wenzelm |
Logic.implies;
|
file |
diff |
annotate
|
| Thu, 19 Jun 2008 20:48:03 +0200 |
wenzelm |
moved add_used to Isar/rule_insts.ML;
|
file |
diff |
annotate
|
| Mon, 16 Jun 2008 22:13:47 +0200 |
wenzelm |
removed obsolete global read_insts/read_instantiate (cf. Isar/rule_insts.ML);
|
file |
diff |
annotate
|
| Wed, 11 Jun 2008 18:03:14 +0200 |
wenzelm |
qualified types_sorts, read_insts etc.;
|
file |
diff |
annotate
|
| Sun, 18 May 2008 15:04:09 +0200 |
wenzelm |
moved global pretty/string_of functions from Sign to Syntax;
|
file |
diff |
annotate
|
| Tue, 15 Apr 2008 16:12:05 +0200 |
wenzelm |
Thm.forall_elim_var(s);
|
file |
diff |
annotate
|
| Sat, 12 Apr 2008 17:00:38 +0200 |
wenzelm |
rep_cterm/rep_thm: no longer dereference theory_ref;
|
file |
diff |
annotate
|
| Sat, 29 Mar 2008 19:14:09 +0100 |
wenzelm |
certify wrt. dynamic context;
|
file |
diff |
annotate
|
| Thu, 27 Mar 2008 14:41:09 +0100 |
wenzelm |
eliminated theory ProtoPure;
|
file |
diff |
annotate
|
| Tue, 27 Nov 2007 15:43:31 +0100 |
berghofe |
Better error messages for cterm_instantiate.
|
file |
diff |
annotate
|
| Thu, 11 Oct 2007 19:10:20 +0200 |
wenzelm |
moved Drule.unvarify to Thm.unvarify (cf. more_thm.ML);
|
file |
diff |
annotate
|
| Wed, 10 Oct 2007 17:31:54 +0200 |
wenzelm |
improved abs_def: only abstract over outermost (unique) Vars;
|
file |
diff |
annotate
|
| Thu, 04 Oct 2007 20:29:24 +0200 |
wenzelm |
replaced literal 'a by Name.aT;
|
file |
diff |
annotate
|
| Fri, 24 Aug 2007 14:17:54 +0200 |
paulson |
new derived rule: incr_type_indexes
|
file |
diff |
annotate
|
| Mon, 13 Aug 2007 18:10:18 +0200 |
wenzelm |
SimpleSyntax.read_prop;
|
file |
diff |
annotate
|
| Sun, 29 Jul 2007 14:30:04 +0200 |
wenzelm |
moved Drule.add/del/merge_rules to Thm.add/del/merge_thms;
|
file |
diff |
annotate
|
| Fri, 27 Jul 2007 20:11:48 +0200 |
wenzelm |
added dummy_thm, is_dummy_thm;
|
file |
diff |
annotate
|
| Wed, 04 Jul 2007 16:49:36 +0200 |
wenzelm |
added binop_cong_rule;
|
file |
diff |
annotate
|
| Tue, 03 Jul 2007 17:17:11 +0200 |
wenzelm |
tuned rotate_prems;
|
file |
diff |
annotate
|
| Wed, 20 Jun 2007 17:32:53 +0200 |
paulson |
A more robust flexflex_unique
|
file |
diff |
annotate
|
| Tue, 19 Jun 2007 23:15:51 +0200 |
wenzelm |
added with_subgoal;
|
file |
diff |
annotate
|
| Thu, 31 May 2007 23:47:36 +0200 |
wenzelm |
simplified/unified list fold;
|
file |
diff |
annotate
|
| Fri, 11 May 2007 18:49:15 +0200 |
wenzelm |
proper type for fun/arg_cong_rule;
|
file |
diff |
annotate
|
| Fri, 11 May 2007 18:47:08 +0200 |
wenzelm |
added fun/arg_cong_rule;
|
file |
diff |
annotate
|
| Thu, 10 May 2007 00:39:52 +0200 |
wenzelm |
moved some operations to more_thm.ML and conv.ML;
|
file |
diff |
annotate
|
| Sun, 15 Apr 2007 14:31:53 +0200 |
wenzelm |
moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
|
file |
diff |
annotate
|
| Sat, 14 Apr 2007 17:36:09 +0200 |
wenzelm |
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
|
file |
diff |
annotate
|
| Mon, 02 Apr 2007 11:31:08 +0200 |
paulson |
optimizing the null instantiation case
|
file |
diff |
annotate
|
| Mon, 26 Feb 2007 23:18:24 +0100 |
wenzelm |
moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
|
file |
diff |
annotate
|
| Tue, 13 Feb 2007 16:37:14 +0100 |
paulson |
COMP now performs a distinctness check on the multiple results before failing
|
file |
diff |
annotate
|
| Sat, 10 Feb 2007 16:43:23 +0100 |
paulson |
Completing the bug fix from the previous update: the result of unifying type
|
file |
diff |
annotate
|
| Thu, 08 Feb 2007 18:14:13 +0100 |
paulson |
cterm_instantiate was calling a type instantiation function that works only for matching,
|
file |
diff |
annotate
|
| Fri, 19 Jan 2007 22:08:18 +0100 |
wenzelm |
moved inst from drule.ML to old_goals.ML;
|
file |
diff |
annotate
|
| Tue, 05 Dec 2006 00:30:38 +0100 |
wenzelm |
thm/prf: separate official name vs. additional tags;
|
file |
diff |
annotate
|
| Thu, 30 Nov 2006 14:17:27 +0100 |
wenzelm |
added zero_var_indexes_list;
|
file |
diff |
annotate
|
| Wed, 29 Nov 2006 23:33:09 +0100 |
wenzelm |
*** bad commit -- reverted to previous version ***
|
file |
diff |
annotate
|
| Wed, 29 Nov 2006 23:28:08 +0100 |
wenzelm |
added INCR_COMP, COMP_INCR;
|
file |
diff |
annotate
|
| Wed, 29 Nov 2006 04:11:11 +0100 |
wenzelm |
added INCR_COMP, COMP_INCR;
|
file |
diff |
annotate
|
| Tue, 28 Nov 2006 00:35:21 +0100 |
wenzelm |
dest_term: strip_imp_concl;
|
file |
diff |
annotate
|
| Fri, 24 Nov 2006 22:05:15 +0100 |
wenzelm |
added cterm_rule;
|
file |
diff |
annotate
|
| Tue, 21 Nov 2006 18:07:33 +0100 |
wenzelm |
moved theorem kinds from PureThy to Thm;
|
file |
diff |
annotate
|
| Mon, 09 Oct 2006 02:19:56 +0200 |
wenzelm |
added dest_equals_lhs;
|
file |
diff |
annotate
|
| Sat, 07 Oct 2006 01:31:09 +0200 |
wenzelm |
added term_rule;
|
file |
diff |
annotate
|
| Thu, 05 Oct 2006 10:40:12 +0200 |
paulson |
a few new functions on thms and cterms
|
file |
diff |
annotate
|
| Thu, 21 Sep 2006 19:04:55 +0200 |
wenzelm |
added dest_equals_rhs;
|
file |
diff |
annotate
|
| Mon, 18 Sep 2006 19:39:07 +0200 |
wenzelm |
Thm.dest_arg;
|
file |
diff |
annotate
|
| Tue, 12 Sep 2006 12:12:46 +0200 |
wenzelm |
moved term subst functions to TermSubst;
|
file |
diff |
annotate
|
| Thu, 03 Aug 2006 17:30:37 +0200 |
wenzelm |
tuned types_sorts, add_used;
|
file |
diff |
annotate
|
| Wed, 02 Aug 2006 22:26:52 +0200 |
wenzelm |
removed obsolete frees/vars_of etc.;
|
file |
diff |
annotate
|
| Sun, 30 Jul 2006 21:28:52 +0200 |
wenzelm |
Thm.adjust_maxidx;
|
file |
diff |
annotate
|
| Thu, 27 Jul 2006 13:43:05 +0200 |
wenzelm |
removed obsolete equal_abs_elim(_list);
|
file |
diff |
annotate
|
| Tue, 11 Jul 2006 12:17:02 +0200 |
wenzelm |
replaced Term.variant(list) by Name.variant(_list);
|
file |
diff |
annotate
|
| Tue, 04 Jul 2006 19:49:50 +0200 |
wenzelm |
added generalize;
|
file |
diff |
annotate
|
| Sat, 17 Jun 2006 19:37:47 +0200 |
wenzelm |
Term.internal;
|
file |
diff |
annotate
|
| Tue, 13 Jun 2006 23:41:44 +0200 |
wenzelm |
removed weak_eq_thm;
|
file |
diff |
annotate
|
| Mon, 12 Jun 2006 21:19:00 +0200 |
wenzelm |
tuned Seq/Envir/Unify interfaces;
|
file |
diff |
annotate
|
| Sun, 11 Jun 2006 21:59:21 +0200 |
wenzelm |
outer_params: Syntax.dest_internal;
|
file |
diff |
annotate
|
| Mon, 05 Jun 2006 21:54:21 +0200 |
wenzelm |
support embedded terms;
|
file |
diff |
annotate
|
| Thu, 01 Jun 2006 14:51:37 +0200 |
paulson |
Tiny code cleanup
|
file |
diff |
annotate
|
| Fri, 26 May 2006 22:20:05 +0200 |
wenzelm |
forall_intr_list: do not ignore errors;
|
file |
diff |
annotate
|
| Mon, 01 May 2006 17:05:11 +0200 |
wenzelm |
added sort_triv;
|
file |
diff |
annotate
|
| Sat, 29 Apr 2006 23:16:46 +0200 |
wenzelm |
added unconstrainTs;
|
file |
diff |
annotate
|
| Thu, 27 Apr 2006 15:06:35 +0200 |
wenzelm |
tuned basic list operators (flat, maps, map_filter);
|
file |
diff |
annotate
|
| Thu, 13 Apr 2006 12:00:59 +0200 |
wenzelm |
added equal_elim_rule2;
|
file |
diff |
annotate
|
| Sat, 04 Mar 2006 21:10:07 +0100 |
wenzelm |
added mk_conjunction;
|
file |
diff |
annotate
|
| Wed, 22 Feb 2006 22:18:38 +0100 |
wenzelm |
removed rename_indexes_wrt;
|
file |
diff |
annotate
|
| Wed, 15 Feb 2006 21:35:02 +0100 |
wenzelm |
added distinct_prems_rl;
|
file |
diff |
annotate
|
| Mon, 06 Feb 2006 20:58:54 +0100 |
wenzelm |
Envir.(beta_)eta_contract;
|
file |
diff |
annotate
|
| Fri, 03 Feb 2006 23:12:30 +0100 |
wenzelm |
removed add/del_rules;
|
file |
diff |
annotate
|
| Sat, 28 Jan 2006 17:28:54 +0100 |
wenzelm |
added equals_cong;
|
file |
diff |
annotate
|
| Fri, 27 Jan 2006 19:03:02 +0100 |
wenzelm |
moved theorem tags from Drule to PureThy;
|
file |
diff |
annotate
|
| Wed, 25 Jan 2006 00:21:35 +0100 |
wenzelm |
abs_def: improved error;
|
file |
diff |
annotate
|
| Sat, 21 Jan 2006 23:02:24 +0100 |
wenzelm |
simplified type attribute;
|
file |
diff |
annotate
|
| Tue, 10 Jan 2006 19:33:32 +0100 |
wenzelm |
added declaration_attribute;
|
file |
diff |
annotate
|
| Sat, 31 Dec 2005 21:49:43 +0100 |
wenzelm |
tuned forall_intr_vars;
|
file |
diff |
annotate
|
| Fri, 23 Dec 2005 15:16:46 +0100 |
wenzelm |
conj_elim_precise: proper treatment of nested conjunctions;
|
file |
diff |
annotate
|
| Thu, 22 Dec 2005 00:28:54 +0100 |
wenzelm |
fixed has_internal;
|
file |
diff |
annotate
|
| Thu, 08 Dec 2005 20:16:10 +0100 |
wenzelm |
removed Syntax.deskolem;
|
file |
diff |
annotate
|
| Fri, 02 Dec 2005 22:54:45 +0100 |
wenzelm |
abs_def: beta/eta contract lhs;
|
file |
diff |
annotate
|
| Fri, 25 Nov 2005 18:58:37 +0100 |
wenzelm |
forall_conv: limit prefix;
|
file |
diff |
annotate
|
| Tue, 22 Nov 2005 19:34:44 +0100 |
wenzelm |
export map_tags;
|
file |
diff |
annotate
|
| Sat, 19 Nov 2005 14:21:03 +0100 |
wenzelm |
removed conj_mono;
|
file |
diff |
annotate
|
| Wed, 16 Nov 2005 17:45:25 +0100 |
wenzelm |
added protect_cong, cong_mono_thm;
|
file |
diff |
annotate
|
| Wed, 09 Nov 2005 16:26:44 +0100 |
wenzelm |
added fold_terms;
|
file |
diff |
annotate
|
| Tue, 08 Nov 2005 10:43:09 +0100 |
wenzelm |
removed impose_hyps, satisfy_hyps;
|
file |
diff |
annotate
|
| Fri, 28 Oct 2005 22:27:52 +0200 |
wenzelm |
added incr_indexes;
|
file |
diff |
annotate
|
| Fri, 21 Oct 2005 18:14:44 +0200 |
wenzelm |
renamed triv_goal to goalI, rev_triv_goal to goalD;
|
file |
diff |
annotate
|
| Thu, 29 Sep 2005 12:30:30 +0200 |
berghofe |
Optimized and exported flexflex_unique.
|
file |
diff |
annotate
|
| Mon, 26 Sep 2005 19:19:14 +0200 |
wenzelm |
moved disambiguate_frees to ProofKernel;
|
file |
diff |
annotate
|
| Mon, 26 Sep 2005 02:06:44 +0200 |
obua |
added Drule.disambiguate_frees : thm -> thm
|
file |
diff |
annotate
|
| Mon, 12 Sep 2005 18:20:32 +0200 |
haftmann |
introduced new-style AList operations
|
file |
diff |
annotate
|
| Wed, 31 Aug 2005 15:46:40 +0200 |
wenzelm |
refer to theory instead of low-level tsig;
|
file |
diff |
annotate
|
| Mon, 01 Aug 2005 19:20:37 +0200 |
wenzelm |
replaced atless by term_ord;
|
file |
diff |
annotate
|
| Thu, 28 Jul 2005 15:20:06 +0200 |
wenzelm |
tuned gen_all, forall_elim_list, implies_intr_list, standard;
|
file |
diff |
annotate
|
| Fri, 15 Jul 2005 15:44:15 +0200 |
wenzelm |
tuned fold on terms;
|
file |
diff |
annotate
|
| Wed, 13 Jul 2005 11:30:37 +0200 |
haftmann |
(fix for an accidental commit)
|
file |
diff |
annotate
|
| Wed, 13 Jul 2005 11:16:34 +0200 |
haftmann |
(intermediate commit)
|
file |
diff |
annotate
|
| Wed, 06 Jul 2005 20:00:25 +0200 |
wenzelm |
Thm.full_prop_of;
|
file |
diff |
annotate
|
| Mon, 04 Jul 2005 17:08:19 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 29 Jun 2005 15:13:25 +0200 |
wenzelm |
added implies_intr_hyps (from thm.ML);
|
file |
diff |
annotate
|
| Fri, 17 Jun 2005 18:33:08 +0200 |
wenzelm |
accomodate identification of type Sign.sg and theory;
|
file |
diff |
annotate
|
| Tue, 10 May 2005 18:37:43 +0200 |
paulson |
new cterm primitives
|
file |
diff |
annotate
|
| Wed, 04 May 2005 18:50:21 +0200 |
berghofe |
Added eta_long_conversion.
|
file |
diff |
annotate
|
| Thu, 28 Apr 2005 21:35:47 +0200 |
wenzelm |
added plain_prop_of;
|
file |
diff |
annotate
|
| Thu, 21 Apr 2005 19:12:03 +0200 |
berghofe |
- Eliminated nodup_vars check.
|
file |
diff |
annotate
|
| Thu, 07 Apr 2005 09:27:20 +0200 |
wenzelm |
added add_used; include tpairs;
|
file |
diff |
annotate
|
| Fri, 04 Mar 2005 15:07:34 +0100 |
skalberg |
Removed practically all references to Library.foldr.
|
file |
diff |
annotate
|
| Thu, 03 Mar 2005 12:43:01 +0100 |
skalberg |
Move towards standard functions.
|
file |
diff |
annotate
|