| Thu, 10 Oct 2019 11:04:27 +0200 |
wenzelm |
unused;
|
file |
diff |
annotate
|
| Wed, 09 Oct 2019 21:59:56 +0200 |
wenzelm |
clarified signature -- some operations to support fully explicit proof terms;
|
file |
diff |
annotate
|
| Mon, 29 Jul 2019 11:38:05 +0200 |
wenzelm |
proper constrains_map -- for shyps that are covered by present variables (amending 251f1fb44ccd);
|
file |
diff |
annotate
|
| Mon, 29 Jul 2019 11:21:41 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 29 Jul 2019 11:09:37 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Mon, 29 Jul 2019 10:26:12 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 20 Jul 2019 12:52:29 +0200 |
wenzelm |
clarified export of sort algebra: avoid logical operations in Isabelle/Scala;
|
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
|
| Sun, 25 Feb 2018 15:44:46 +0100 |
wenzelm |
eliminated ASCII syntax from Pure bootstrap;
|
file |
diff |
annotate
|
| Wed, 27 Apr 2016 10:03:35 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 26 Apr 2016 16:20:28 +0200 |
wenzelm |
defs are closed, which leads to proper auto_bind_facts;
|
file |
diff |
annotate
|
| Fri, 13 Nov 2015 14:11:54 +0100 |
wenzelm |
avoid vacuous quantification, as usual for shared variable scope;
|
file |
diff |
annotate
|
| Fri, 13 Nov 2015 11:41:11 +0100 |
wenzelm |
support for structure statements in 'assume', 'presume';
|
file |
diff |
annotate
|
| Thu, 09 Jul 2015 22:08:20 +0200 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Sat, 13 Jun 2015 16:35:27 +0200 |
wenzelm |
eliminated slightly odd Element.close_form: toplevel specifications have different policies than proof text elements;
|
file |
diff |
annotate
|
| Mon, 23 Mar 2015 19:43:03 +0100 |
wenzelm |
local fixes may depend on goal params;
|
file |
diff |
annotate
|
| Fri, 21 Mar 2014 20:33:56 +0100 |
wenzelm |
more qualified names;
|
file |
diff |
annotate
|
| Fri, 21 Mar 2014 15:12:03 +0100 |
wenzelm |
more qualified names;
|
file |
diff |
annotate
|
| Fri, 21 Mar 2014 12:34:50 +0100 |
wenzelm |
more qualified names;
|
file |
diff |
annotate
|
| 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
|
| Mon, 21 Jan 2008 14:18:49 +0100 |
berghofe |
Removed Logic.auto_rename.
|
file |
diff |
annotate
|
| Thu, 04 Oct 2007 20:29:24 +0200 |
wenzelm |
replaced literal 'a by Name.aT;
|
file |
diff |
annotate
|
| Tue, 14 Aug 2007 13:20:16 +0200 |
wenzelm |
moved support for primitive defs to primitive_defs.ML;
|
file |
diff |
annotate
|
| Thu, 05 Jul 2007 20:01:34 +0200 |
wenzelm |
simplified has_meta_prems;
|
file |
diff |
annotate
|
| Tue, 19 Jun 2007 23:15:27 +0200 |
wenzelm |
balanced conjunctions;
|
file |
diff |
annotate
|
| Wed, 13 Jun 2007 00:02:00 +0200 |
wenzelm |
removed unused is_atomic;
|
file |
diff |
annotate
|
| Mon, 04 Jun 2007 21:04:19 +0200 |
wenzelm |
added is_atomic;
|
file |
diff |
annotate
|
| Wed, 09 May 2007 19:37:18 +0200 |
wenzelm |
removed unused mk_cond_defpair;
|
file |
diff |
annotate
|
| Wed, 29 Nov 2006 04:11:09 +0100 |
wenzelm |
simplified Logic.count_prems;
|
file |
diff |
annotate
|
| Fri, 24 Nov 2006 22:05:16 +0100 |
wenzelm |
added type_map;
|
file |
diff |
annotate
|
| Fri, 13 Oct 2006 18:08:48 +0200 |
berghofe |
Repaired strip_assums_hyp (now also works for goals not
|
file |
diff |
annotate
|
| Sat, 07 Oct 2006 01:31:11 +0200 |
wenzelm |
removed is_equals, is_implies;
|
file |
diff |
annotate
|
| Tue, 19 Sep 2006 23:15:39 +0200 |
wenzelm |
added name_classrel/arities/arity;
|
file |
diff |
annotate
|
| Fri, 15 Sep 2006 22:56:13 +0200 |
wenzelm |
renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
|
file |
diff |
annotate
|
| Tue, 11 Jul 2006 12:17:03 +0200 |
wenzelm |
replaced Term.variant(list) by Name.variant(_list);
|
file |
diff |
annotate
|
| Tue, 13 Jun 2006 23:41:47 +0200 |
wenzelm |
(un)varify: tuned exceptions;
|
file |
diff |
annotate
|
| Wed, 07 Jun 2006 02:01:28 +0200 |
wenzelm |
renamed Type.(un)varifyT to Logic.(un)varifyT;
|
file |
diff |
annotate
|
| Mon, 05 Jun 2006 21:54:21 +0200 |
wenzelm |
support embedded terms;
|
file |
diff |
annotate
|
| Thu, 13 Apr 2006 12:01:03 +0200 |
wenzelm |
added dest_conjunction_list;
|
file |
diff |
annotate
|
| Tue, 11 Apr 2006 16:00:02 +0200 |
wenzelm |
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
|
file |
diff |
annotate
|
| Mon, 10 Apr 2006 00:33:49 +0200 |
wenzelm |
Term.itselfT;
|
file |
diff |
annotate
|
| Wed, 22 Feb 2006 22:18:39 +0100 |
wenzelm |
simplified Pure conjunction, based on actual const;
|
file |
diff |
annotate
|
| Sat, 18 Feb 2006 18:08:23 +0100 |
wenzelm |
dest_def: tuned error msg;
|
file |
diff |
annotate
|
| Thu, 16 Feb 2006 18:25:55 +0100 |
wenzelm |
dest_def: actually return beta-eta contracted equation;
|
file |
diff |
annotate
|
| Tue, 07 Feb 2006 19:56:45 +0100 |
wenzelm |
renamed gen_duplicates to duplicates;
|
file |
diff |
annotate
|
| Mon, 06 Feb 2006 20:59:05 +0100 |
wenzelm |
added generic dest_def (mostly from theory.ML);
|
file |
diff |
annotate
|
| Tue, 24 Jan 2006 00:43:23 +0100 |
wenzelm |
added dest_all;
|
file |
diff |
annotate
|
| Fri, 23 Dec 2005 15:16:48 +0100 |
wenzelm |
added mk_conjunction_list2;
|
file |
diff |
annotate
|
| Thu, 22 Dec 2005 00:28:58 +0100 |
wenzelm |
mk_conjunction: proper treatment of bounds;
|
file |
diff |
annotate
|
| Fri, 25 Nov 2005 18:58:34 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 16 Nov 2005 17:45:27 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 28 Oct 2005 22:27:57 +0200 |
wenzelm |
renamed Goal constant to prop, more general protect/unprotect interfaces;
|
file |
diff |
annotate
|
| Thu, 18 Aug 2005 13:06:05 +0200 |
paulson |
optimization to incr_indexes?
|
file |
diff |
annotate
|
| Tue, 19 Jul 2005 17:21:51 +0200 |
wenzelm |
incr_tvar (from term.ML), incr_indexes: avoid garbage;
|
file |
diff |
annotate
|
| Fri, 15 Jul 2005 15:44:17 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 14 Jul 2005 19:28:29 +0200 |
wenzelm |
occs no longer infix (structure not open);
|
file |
diff |
annotate
|
| Tue, 31 May 2005 11:53:21 +0200 |
wenzelm |
added nth_prem;
|
file |
diff |
annotate
|
| Wed, 09 Mar 2005 18:44:52 +0100 |
ballarin |
First version of global registration command.
|
file |
diff |
annotate
|
| Mon, 24 Jan 2005 12:41:06 +0100 |
paulson |
thin_tac now works on P==>Q
|
file |
diff |
annotate
|
| Fri, 21 Jan 2005 13:55:07 +0100 |
paulson |
fixed thin_tac with higher-level assumptions by removing the old code to
|
file |
diff |
annotate
|
| Thu, 31 Jul 2003 00:01:47 +0200 |
berghofe |
Removed extraneous rev in function goal_params (the list of parameters
|
file |
diff |
annotate
|
| Fri, 11 Jul 2003 15:00:10 +0200 |
berghofe |
Exported function goal_params.
|
file |
diff |
annotate
|
| Mon, 03 Feb 2003 11:04:16 +0100 |
berghofe |
Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
|
file |
diff |
annotate
|
| Mon, 21 Oct 2002 17:07:27 +0200 |
berghofe |
Removed obsolete functions dealing with flex-flex constraints.
|
file |
diff |
annotate
|
| Wed, 20 Feb 2002 00:53:53 +0100 |
wenzelm |
Symbol.bump_string;
|
file |
diff |
annotate
|
| Thu, 17 Jan 2002 20:59:46 +0100 |
wenzelm |
is_norm_hhf moved to drule.ML;
|
file |
diff |
annotate
|
| Tue, 15 Jan 2002 00:09:54 +0100 |
wenzelm |
added mk_conjunction_list;
|
file |
diff |
annotate
|
| Sun, 11 Nov 2001 21:30:51 +0100 |
wenzelm |
added mk_conjunction;
|
file |
diff |
annotate
|
| Sun, 07 Jan 2001 21:35:34 +0100 |
wenzelm |
added is_norm_hhf;
|
file |
diff |
annotate
|
| Fri, 10 Nov 2000 19:10:34 +0100 |
wenzelm |
has_meta_prems: include "==";
|
file |
diff |
annotate
|
| Thu, 24 Aug 2000 11:14:21 +0200 |
paulson |
fixed strip_assums and assum_pairs, restoring them (essentially) to their
|
file |
diff |
annotate
|
| Mon, 21 Aug 2000 18:16:47 +0200 |
wenzelm |
fixed has_meta_prems: strip_assums_hyp;
|
file |
diff |
annotate
|
| Tue, 01 Aug 2000 00:19:07 +0200 |
wenzelm |
added has_meta_prems;
|
file |
diff |
annotate
|
| Sun, 30 Jul 2000 12:48:55 +0200 |
wenzelm |
Logic.goal_const;
|
file |
diff |
annotate
|
| Wed, 17 Jun 1998 10:48:38 +0200 |
nipkow |
Goals may now contain assumptions, which are not returned.
|
file |
diff |
annotate
|
| Wed, 22 Apr 1998 19:08:49 +0200 |
wenzelm |
added mk_cond_defpair, mk_defpair;
|
file |
diff |
annotate
|
| Mon, 09 Mar 1998 16:09:06 +0100 |
wenzelm |
adapted to baroque chars;
|
file |
diff |
annotate
|
| Wed, 04 Mar 1998 13:16:05 +0100 |
nipkow |
Reorganized simplifier. May now reorient rules.
|
file |
diff |
annotate
|
| Sat, 28 Feb 1998 15:40:03 +0100 |
nipkow |
Tried to reorganize rewriter a little. More to be done.
|
file |
diff |
annotate
|
| Wed, 18 Feb 1998 11:31:25 +0100 |
nipkow |
Improved loop-test for rewrite rules a little.
|
file |
diff |
annotate
|
| Fri, 19 Dec 1997 10:15:51 +0100 |
wenzelm |
term order stuff moved to term.ML;
|
file |
diff |
annotate
|
| Tue, 02 Dec 1997 12:42:28 +0100 |
wenzelm |
tuned term order;
|
file |
diff |
annotate
|
| Fri, 28 Nov 1997 07:35:10 +0100 |
nipkow |
Fixed the definition of `termord': is now antisymmetric.
|
file |
diff |
annotate
|
| Tue, 04 Nov 1997 12:58:10 +0100 |
nipkow |
logic: loops -> rewrite_rule_ok
|
file |
diff |
annotate
|
| Tue, 21 Oct 1997 17:36:54 +0200 |
nipkow |
Corrected alphabetical order of entries in signature.
|
file |
diff |
annotate
|
| Fri, 17 Oct 1997 11:10:13 +0200 |
paulson |
Added "op" before "occs" to make sml/nj happy
|
file |
diff |
annotate
|
| Thu, 16 Oct 1997 13:45:16 +0200 |
nipkow |
The simplifier has been improved a little: equations s=t which used to be
|
file |
diff |
annotate
|
| Thu, 05 Jun 1997 13:30:24 +0200 |
paulson |
Removal of freeze_vars and thaw_vars (quite unused...)
|
file |
diff |
annotate
|
| Thu, 16 Jan 1997 13:44:47 +0100 |
wenzelm |
added term order;
|
file |
diff |
annotate
|
| Thu, 28 Nov 1996 10:44:24 +0100 |
paulson |
Replaced map...~~ by ListPair.map
|
file |
diff |
annotate
|
| Fri, 28 Jun 1996 11:10:32 +0200 |
paulson |
Restored warning comment
|
file |
diff |
annotate
|