| Tue, 16 Oct 2012 17:47:23 +0200 |
wenzelm |
clarified defer/prefer: more specific errors;
|
file |
diff |
annotate
|
| Sat, 14 Jan 2012 20:05:58 +0100 |
wenzelm |
renamed Term.list_all to Logic.list_all, in accordance to HOLogic.list_all;
|
file |
diff |
annotate
|
| Sat, 14 Jan 2012 19:06:05 +0100 |
wenzelm |
renamed Term.all to Logic.all_const, in accordance to HOLogic.all_const;
|
file |
diff |
annotate
|
| Sat, 14 Jan 2012 17:45:04 +0100 |
wenzelm |
discontinued old-style Term.list_all_free in favour of plain Logic.all;
|
file |
diff |
annotate
|
| Sat, 05 Nov 2011 15:00:49 +0100 |
wenzelm |
added Logic.varify_types_global/unvarify_types_global, which avoids somewhat expensive Term.map_types;
|
file |
diff |
annotate
|
| Thu, 03 Nov 2011 22:51:37 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 20:22:22 +0200 |
wenzelm |
tuned signature: Name.invent and Name.invent_names;
|
file |
diff |
annotate
|
| Tue, 01 Jun 2010 10:55:38 +0200 |
berghofe |
outer_constraints with original variable names, to ensure that argsP is consistent with args
|
file |
diff |
annotate
|
| Sun, 09 May 2010 19:15:21 +0200 |
wenzelm |
just one version of Thm.unconstrainT, which affects all variables;
|
file |
diff |
annotate
|
| Sun, 09 May 2010 18:09:30 +0200 |
wenzelm |
added Logic.unconstrain_allTs, based on calculations_for_thm_proof by krauss/schropp, but treat type variables uniformly as in strip_shyps (in thm.ML) or stripped_sorts (in more_thm.ML);
|
file |
diff |
annotate
|
| Sun, 21 Mar 2010 22:13:31 +0100 |
wenzelm |
Logic.mk_of_sort convenience;
|
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
|
| Wed, 30 Sep 2009 22:20:58 +0200 |
wenzelm |
eliminated redundant bindings;
|
file |
diff |
annotate
|
| Tue, 29 Sep 2009 22:48:24 +0200 |
wenzelm |
modernized Balanced_Tree;
|
file |
diff |
annotate
|
| Thu, 16 Jul 2009 22:58:07 +0200 |
wenzelm |
tuned incr_tvar_same;
|
file |
diff |
annotate
|
| Thu, 16 Jul 2009 21:29:02 +0200 |
wenzelm |
export incr_tvar_same;
|
file |
diff |
annotate
|
| Thu, 16 Jul 2009 21:00:09 +0200 |
wenzelm |
use structure Same;
|
file |
diff |
annotate
|
| Thu, 16 Jul 2009 00:24:11 +0200 |
wenzelm |
removed obsolete/unused legacy_varify;
|
file |
diff |
annotate
|
| Wed, 15 Jul 2009 21:42:24 +0200 |
wenzelm |
tuned comment;
|
file |
diff |
annotate
|
| Tue, 14 Jul 2009 12:18:52 +0200 |
wenzelm |
removed obsolete/unused legacy_unvarify;
|
file |
diff |
annotate
|
| Fri, 10 Jul 2009 00:47:17 +0200 |
wenzelm |
tuned varify/unvarify: use Term_Subst.map_XXX combinators;
|
file |
diff |
annotate
|
| Mon, 06 Jul 2009 19:58:52 +0200 |
wenzelm |
renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
|
file |
diff |
annotate
|
| Mon, 16 Mar 2009 23:52:30 +0100 |
wenzelm |
substantial speedup of assumption and elim-resolution: Logic.assum_problems refrains from eager application of parameters, discriminate via Term.could_unify before invoking full unification (assumes terms in beta-normal form, as do higher term net operations anyway);
|
file |
diff |
annotate
|
| Sun, 08 Mar 2009 17:26:14 +0100 |
wenzelm |
moved basic algebra of long names from structure NameSpace to Long_Name;
|
file |
diff |
annotate
|
| Thu, 05 Mar 2009 12:08:00 +0100 |
wenzelm |
renamed NameSpace.base to NameSpace.base_name;
|
file |
diff |
annotate
|
| Wed, 31 Dec 2008 19:54:03 +0100 |
wenzelm |
qualified Term.rename_wrt_term;
|
file |
diff |
annotate
|
| Thu, 20 Nov 2008 00:03:47 +0100 |
wenzelm |
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
|
file |
diff |
annotate
|
| Wed, 01 Oct 2008 14:17:06 +0200 |
wenzelm |
tuned comments;
|
file |
diff |
annotate
|
| Mon, 23 Jun 2008 23:45:47 +0200 |
wenzelm |
added all, is_all;
|
file |
diff |
annotate
|
| Thu, 27 Mar 2008 14:41:09 +0100 |
wenzelm |
eliminated theory ProtoPure;
|
file |
diff |
annotate
|