| Wed, 29 May 2013 18:25:11 +0200 |
wenzelm |
tuned signature -- more explicit flags for low-level Thm.bicompose;
|
file |
diff |
annotate
|
| Mon, 20 May 2013 17:14:39 +0200 |
wenzelm |
more precise treatment of theory vs. Proof.context;
|
file |
diff |
annotate
|
| Wed, 03 Apr 2013 16:45:14 +0200 |
wenzelm |
tuned -- Drule.comp_no_flatten includes Drule.incr_indexes already (NB: result should be deterministic by construction);
|
file |
diff |
annotate
|
| Mon, 26 Nov 2012 21:46:04 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 11 Nov 2012 20:31:46 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 16 Oct 2012 17:47:23 +0200 |
wenzelm |
clarified defer/prefer: more specific errors;
|
file |
diff |
annotate
|
| Mon, 27 Feb 2012 15:00:19 +0100 |
wenzelm |
simplified cut_tac (cf. d549b5b0f344);
|
file |
diff |
annotate
|
| Tue, 14 Feb 2012 21:31:26 +0100 |
wenzelm |
eliminated odd/obsolete innermost_params (cf. a77ad6c86564, 3458b0e955ac);
|
file |
diff |
annotate
|
| Tue, 14 Feb 2012 17:11:33 +0100 |
wenzelm |
eliminated obsolete aliases;
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 16:34:14 +0200 |
wenzelm |
discontinued special treatment of structure Lexicon;
|
file |
diff |
annotate
|
| Sat, 15 May 2010 21:41:32 +0200 |
wenzelm |
less pervasive names from structure Thm;
|
file |
diff |
annotate
|
| Fri, 30 Apr 2010 18:06:29 +0200 |
wenzelm |
proper context for rule_by_tactic;
|
file |
diff |
annotate
|
| Mon, 26 Apr 2010 20:30:50 +0200 |
wenzelm |
eliminanated some unreferenced identifiers;
|
file |
diff |
annotate
|
| Sat, 06 Mar 2010 14:35:06 +0100 |
wenzelm |
removed unused term_lift_inst_rule (superceded by Subgoal.FOCUS etc.);
|
file |
diff |
annotate
|
| Wed, 25 Nov 2009 09:13:46 +0100 |
haftmann |
normalized uncurry take/drop
|
file |
diff |
annotate
|
| Tue, 24 Nov 2009 17:28:25 +0100 |
haftmann |
curried take/drop
|
file |
diff |
annotate
|
| Sat, 17 Oct 2009 17:18:59 +0200 |
wenzelm |
less pervasive names;
|
file |
diff |
annotate
|
| Mon, 06 Jul 2009 21:24:30 +0200 |
wenzelm |
structure Thm: less pervasive names;
|
file |
diff |
annotate
|
| Wed, 24 Jun 2009 21:28:02 +0200 |
wenzelm |
renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef -- Alice is no longer supported);
|
file |
diff |
annotate
|
| Sun, 24 May 2009 15:02:23 +0200 |
haftmann |
tuned whitespace
|
file |
diff |
annotate
|
| Tue, 17 Mar 2009 14:09:20 +0100 |
wenzelm |
renamed Tactic.taglist/untaglist/orderlist to tag_list/untag_list/order_list (in library.ML);
|
file |
diff |
annotate
|
| Wed, 31 Dec 2008 19:54:03 +0100 |
wenzelm |
qualified Term.rename_wrt_term;
|
file |
diff |
annotate
|
| Mon, 16 Jun 2008 22:13:50 +0200 |
wenzelm |
removed obsolete global instantiation tactics (cf. Isar/rule_insts.ML);
|
file |
diff |
annotate
|
| Sat, 14 Jun 2008 23:19:57 +0200 |
wenzelm |
qualified old res_inst_tac variants;
|
file |
diff |
annotate
|
| Wed, 11 Jun 2008 18:04:02 +0200 |
wenzelm |
Drule.read_instantiate;
|
file |
diff |
annotate
|
| Sat, 12 Apr 2008 17:00:35 +0200 |
wenzelm |
rep_cterm/rep_thm: no longer dereference theory_ref;
|
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
|
| Mon, 13 Aug 2007 18:10:22 +0200 |
wenzelm |
Lexicon.read_indexname/nat/variable;
|
file |
diff |
annotate
|
| Tue, 03 Jul 2007 17:17:13 +0200 |
wenzelm |
removed obsolete eta_long_tac;
|
file |
diff |
annotate
|
| Mon, 25 Jun 2007 00:36:41 +0200 |
wenzelm |
added eta_long_tac;
|
file |
diff |
annotate
|
| Sun, 03 Jun 2007 23:16:51 +0200 |
wenzelm |
cleaned up signature;
|
file |
diff |
annotate
|
| Thu, 31 May 2007 23:47:36 +0200 |
wenzelm |
simplified/unified list fold;
|
file |
diff |
annotate
|
| Wed, 04 Apr 2007 00:11:14 +0200 |
wenzelm |
added scanwords from library.ML (for obsolete rename_tac);
|
file |
diff |
annotate
|
| Tue, 03 Apr 2007 19:24:13 +0200 |
wenzelm |
renamed Variable.import to import_thms (avoid clash with Alice keywords);
|
file |
diff |
annotate
|
| Mon, 02 Apr 2007 11:30:44 +0200 |
paulson |
now exports distinct_subgoal_tac (needed by MetisAPI)
|
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
|
| Thu, 07 Dec 2006 23:16:55 +0100 |
wenzelm |
reorganized structure Tactic vs. MetaSimplifier;
|
file |
diff |
annotate
|
| Thu, 07 Dec 2006 00:42:04 +0100 |
wenzelm |
reorganized structure Goal vs. Tactic;
|
file |
diff |
annotate
|
| Wed, 02 Aug 2006 22:26:56 +0200 |
wenzelm |
renamed Syntax.indexname to Syntax.read_indexname;
|
file |
diff |
annotate
|
| Thu, 27 Jul 2006 13:43:10 +0200 |
wenzelm |
removed obsolete is_fact (cf. Thm.no_prems);
|
file |
diff |
annotate
|
| Wed, 26 Jul 2006 19:37:41 +0200 |
wenzelm |
Variable.import(T): result includes fixed types/terms;
|
file |
diff |
annotate
|
| Wed, 12 Jul 2006 21:19:19 +0200 |
wenzelm |
exported make_elim_preserve;
|
file |
diff |
annotate
|
| Mon, 19 Jun 2006 20:21:30 +0200 |
wenzelm |
eliminated freeze/varify in favour of Variable.import/export/trade;
|
file |
diff |
annotate
|
| Mon, 29 May 2006 13:15:53 +0200 |
paulson |
fixing a variable-clash bug in rule_by_tactic
|
file |
diff |
annotate
|
| Tue, 02 May 2006 14:27:49 +0200 |
paulson |
tidied and harmonized "params_of_state"
|
file |
diff |
annotate
|
| Thu, 27 Apr 2006 15:06:35 +0200 |
wenzelm |
tuned basic list operators (flat, maps, map_filter);
|
file |
diff |
annotate
|
| Wed, 26 Apr 2006 22:38:05 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 13 Apr 2006 12:01:01 +0200 |
wenzelm |
use conjunction stuff from conjunction.ML;
|
file |
diff |
annotate
|
| Sat, 04 Mar 2006 21:10:09 +0100 |
wenzelm |
tuned conj_curry;
|
file |
diff |
annotate
|
| Wed, 22 Feb 2006 22:18:39 +0100 |
wenzelm |
simplified Pure conjunction, based on actual const;
|
file |
diff |
annotate
|
| Wed, 15 Feb 2006 21:35:06 +0100 |
wenzelm |
sane version of distinct_subgoals_tac, based on composition with Drule.distinct_prems_rl;
|
file |
diff |
annotate
|
| Wed, 08 Feb 2006 14:39:00 +0100 |
haftmann |
introduced gen_distinct in place of distinct
|
file |
diff |
annotate
|
| Fri, 23 Dec 2005 15:16:49 +0100 |
wenzelm |
CONJUNCTS: full nesting (again), PRECISE_CONJUNCTS: outer level of nesting;
|
file |
diff |
annotate
|
| Thu, 22 Dec 2005 00:29:01 +0100 |
wenzelm |
conjunction_tac: single goal;
|
file |
diff |
annotate
|
| Sat, 19 Nov 2005 14:21:06 +0100 |
wenzelm |
added CONJUNCTS: treat conjunction as separate sub-goals;
|
file |
diff |
annotate
|
| Thu, 10 Nov 2005 20:57:11 +0100 |
wenzelm |
renamed Thm.cgoal_of to Thm.cprem_of;
|
file |
diff |
annotate
|
| Fri, 28 Oct 2005 22:28:03 +0200 |
wenzelm |
accomodate simplified Thm.lift_rule;
|
file |
diff |
annotate
|
| Fri, 21 Oct 2005 18:14:48 +0200 |
wenzelm |
moved norm_hhf_rule, prove etc. to goal.ML;
|
file |
diff |
annotate
|
| Tue, 18 Oct 2005 17:59:25 +0200 |
wenzelm |
Simplifier.theory_context;
|
file |
diff |
annotate
|
| Sat, 15 Oct 2005 00:08:00 +0200 |
wenzelm |
tuned comments;
|
file |
diff |
annotate
|
| Tue, 20 Sep 2005 08:21:49 +0200 |
haftmann |
slight adaptions to library changes
|
file |
diff |
annotate
|
| Tue, 06 Sep 2005 08:30:43 +0200 |
haftmann |
introduced some 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
|
| Thu, 28 Jul 2005 15:19:59 +0200 |
wenzelm |
norm_hhf_rule: Thm.adjust_maxidx_thm before Drule.gen_all;
|
file |
diff |
annotate
|
| Tue, 19 Jul 2005 17:21:47 +0200 |
wenzelm |
Logic.incr_tvar;
|
file |
diff |
annotate
|
| Wed, 13 Jul 2005 16:07:30 +0200 |
wenzelm |
export eq_brl;
|
file |
diff |
annotate
|
| Fri, 01 Jul 2005 22:34:50 +0200 |
wenzelm |
cterm_aconv: avoid rep_cterm;
|
file |
diff |
annotate
|
| Fri, 17 Jun 2005 18:33:08 +0200 |
wenzelm |
accomodate identification of type Sign.sg and theory;
|
file |
diff |
annotate
|
| Wed, 08 Jun 2005 16:11:09 +0200 |
ballarin |
Fixed "axiom" generation for mixed locales with and without predicates.
|
file |
diff |
annotate
|
| Tue, 17 May 2005 17:01:35 +0200 |
paulson |
added comment
|
file |
diff |
annotate
|
| Thu, 28 Apr 2005 21:35:25 +0200 |
wenzelm |
added smart_conjunction_tac, prove_multi, prove_multi_standard;
|
file |
diff |
annotate
|
| Thu, 21 Apr 2005 19:12:03 +0200 |
berghofe |
- Eliminated nodup_vars check.
|
file |
diff |
annotate
|
| Mon, 11 Apr 2005 12:34:34 +0200 |
ballarin |
First release of interpretation commands.
|
file |
diff |
annotate
|
| Thu, 07 Apr 2005 09:27:50 +0200 |
wenzelm |
Drule.add_used;
|
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
|
| Sun, 13 Feb 2005 17:15:14 +0100 |
skalberg |
Deleted Library.option type.
|
file |
diff |
annotate
|
| Mon, 24 Jan 2005 18:18:28 +0100 |
berghofe |
Added variant of eres_inst_tac that operates on indexnames instead of strings.
|
file |
diff |
annotate
|
| Mon, 24 Jan 2005 12:40:52 +0100 |
paulson |
some rationalizing of res_inst_tac
|
file |
diff |
annotate
|
| Tue, 18 Jan 2005 14:34:24 +0100 |
berghofe |
Added variants of instantiation functions that operate on pairs of type
|
file |
diff |
annotate
|
| Thu, 08 Jul 2004 19:33:05 +0200 |
wenzelm |
got rid of obsolete meta_simpset;
|
file |
diff |
annotate
|
| Wed, 30 Jun 2004 00:42:59 +0200 |
skalberg |
Made simplification procedures simpset-aware.
|
file |
diff |
annotate
|
| Fri, 25 Jun 2004 14:30:55 +0200 |
skalberg |
Merging the meta-simplifier with the Provers-simplifier. Next step:
|
file |
diff |
annotate
|
| Mon, 26 Apr 2004 14:54:45 +0200 |
wenzelm |
use Syntax.is_identifier;
|
file |
diff |
annotate
|
| Sat, 26 Apr 2003 12:38:17 +0200 |
paulson |
catches exception DELETE
|
file |
diff |
annotate
|
| Thu, 17 Oct 2002 10:52:59 +0200 |
paulson |
fixing the cut_tac method to work when there are no instantiations and the
|
file |
diff |
annotate
|
| Thu, 05 Sep 2002 14:03:03 +0200 |
paulson |
added checking so that (rename_tac "x y") is rejected, since
|
file |
diff |
annotate
|
| Tue, 07 May 2002 14:26:32 +0200 |
wenzelm |
use eq_thm_prop instead of slightly inadequate eq_thm;
|
file |
diff |
annotate
|
| Thu, 24 Jan 2002 22:42:14 +0100 |
wenzelm |
fixed subgoal_tac; fails on non-existent subgoal;
|
file |
diff |
annotate
|
| Thu, 17 Jan 2002 21:03:29 +0100 |
wenzelm |
renamed norm_hhf to norm_hhf_rule;
|
file |
diff |
annotate
|
| Wed, 16 Jan 2002 22:24:37 +0100 |
wenzelm |
tune norm_hhf_tac;
|
file |
diff |
annotate
|
| Sat, 12 Jan 2002 16:37:58 +0100 |
wenzelm |
renamed forall_elim_vars_safe to gen_all;
|
file |
diff |
annotate
|
| Fri, 14 Dec 2001 11:52:54 +0100 |
wenzelm |
changed Thm.varifyT';
|
file |
diff |
annotate
|
| Thu, 29 Nov 2001 00:44:34 +0100 |
wenzelm |
general type of delete_tagged_brl;
|
file |
diff |
annotate
|
| Wed, 21 Nov 2001 00:36:51 +0100 |
wenzelm |
use tracing function for trace output;
|
file |
diff |
annotate
|
| Thu, 15 Nov 2001 18:36:07 +0100 |
wenzelm |
prove: raise ERROR_MESSAGE;
|
file |
diff |
annotate
|
| Tue, 13 Nov 2001 17:51:03 +0100 |
wenzelm |
prove: Envir.beta_norm;
|
file |
diff |
annotate
|
| Sun, 11 Nov 2001 21:31:52 +0100 |
wenzelm |
added conjunction_tac;
|
file |
diff |
annotate
|
| Sun, 28 Oct 2001 19:44:26 +0100 |
wenzelm |
tuned prove;
|
file |
diff |
annotate
|
| Sat, 27 Oct 2001 23:19:04 +0200 |
wenzelm |
tuned prove;
|
file |
diff |
annotate
|
| Sat, 27 Oct 2001 00:07:19 +0200 |
wenzelm |
prove: primitive goal interface for internal use;
|
file |
diff |
annotate
|
| Thu, 25 Oct 2001 02:12:10 +0200 |
wenzelm |
innermost_params;
|
file |
diff |
annotate
|
| Mon, 15 Oct 2001 20:31:52 +0200 |
wenzelm |
qualify some names;
|
file |
diff |
annotate
|
| Sun, 14 Oct 2001 22:05:46 +0200 |
wenzelm |
unified rewrite/rewrite_cterm/simplify interface;
|
file |
diff |
annotate
|
| Sun, 14 Oct 2001 20:08:42 +0200 |
wenzelm |
tuned full_rewrite;
|
file |
diff |
annotate
|
| Thu, 04 Oct 2001 15:21:17 +0200 |
wenzelm |
added full_rewrite_cterm;
|
file |
diff |
annotate
|
| Sun, 07 Jan 2001 21:36:11 +0100 |
wenzelm |
tuned norm_hhf(_tac);
|
file |
diff |
annotate
|
| Sat, 06 Jan 2001 21:27:12 +0100 |
wenzelm |
added norm_hhf(_tac);
|
file |
diff |
annotate
|
| Fri, 10 Nov 2000 19:12:30 +0100 |
wenzelm |
added rewrite_goal_tac;
|
file |
diff |
annotate
|
| Tue, 07 Nov 2000 17:50:21 +0100 |
berghofe |
moved rewriting functions from Drule to MetaSimplifier
|
file |
diff |
annotate
|
| Fri, 27 Oct 2000 15:53:47 +0200 |
oheimb |
added instantiate_tac
|
file |
diff |
annotate
|
| Fri, 04 Aug 2000 22:59:08 +0200 |
wenzelm |
added rename_params_tac;
|
file |
diff |
annotate
|
| Thu, 25 May 2000 15:22:19 +0200 |
paulson |
res_inst_tac, etc., no longer print the "dest_state" message when the selected
|
file |
diff |
annotate
|
| Mon, 17 Jan 2000 14:10:32 +0100 |
paulson |
Thm.instantiate no longer normalizes, but Drule.instantiate does
|
file |
diff |
annotate
|
| Sat, 25 Sep 1999 13:05:38 +0200 |
wenzelm |
added fold_rule;
|
file |
diff |
annotate
|
| Mon, 06 Sep 1999 18:18:09 +0200 |
oheimb |
added ftac, eatac, datac, fatac
|
file |
diff |
annotate
|
| Wed, 18 Aug 1999 10:54:44 +0200 |
paulson |
new primitive rule permute_prems to underlie defer_tac and rotate_prems
|
file |
diff |
annotate
|
| Mon, 12 Jul 1999 22:25:19 +0200 |
wenzelm |
removed metacuts_tac;
|
file |
diff |
annotate
|
| Sat, 10 Jul 1999 21:41:57 +0200 |
wenzelm |
defer_tac: use try for general exn handling;
|
file |
diff |
annotate
|