Fri, 28 Oct 2011 22:17:30 +0200 |
wenzelm |
uniform Local_Theory.declaration with explicit params;
|
file |
diff |
annotate
|
Fri, 28 Oct 2011 17:15:52 +0200 |
wenzelm |
tuned signature -- refined terminology;
|
file |
diff |
annotate
|
Mon, 08 Aug 2011 17:23:15 +0200 |
wenzelm |
misc tuning -- eliminated old-fashioned rep_thm;
|
file |
diff |
annotate
|
Wed, 29 Jun 2011 21:34:16 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Wed, 29 Jun 2011 20:39:41 +0200 |
wenzelm |
simplified/unified Simplifier.mk_solver;
|
file |
diff |
annotate
|
Mon, 27 Jun 2011 16:53:31 +0200 |
wenzelm |
ML antiquotations are managed as theory data, with proper name space and entity markup;
|
file |
diff |
annotate
|
Fri, 13 May 2011 23:58:40 +0200 |
wenzelm |
clarified map_simpset versus Simplifier.map_simpset_global;
|
file |
diff |
annotate
|
Fri, 13 May 2011 22:55:00 +0200 |
wenzelm |
proper Proof.context for classical tactics;
|
file |
diff |
annotate
|
Sat, 23 Apr 2011 17:02:12 +0200 |
wenzelm |
added Name_Space.check/get convenience;
|
file |
diff |
annotate
|
Sat, 23 Apr 2011 16:30:00 +0200 |
wenzelm |
clarified check_simproc (with report) vs. the_simproc;
|
file |
diff |
annotate
|
Sat, 23 Apr 2011 13:53:09 +0200 |
wenzelm |
proper binding/report of defined simprocs;
|
file |
diff |
annotate
|
Sun, 17 Apr 2011 19:54:04 +0200 |
wenzelm |
report Name_Space.declare/define, relatively to context;
|
file |
diff |
annotate
|
Sat, 16 Apr 2011 23:41:25 +0200 |
wenzelm |
PARALLEL_GOALS for method "simp_all";
|
file |
diff |
annotate
|
Sat, 16 Apr 2011 15:47:52 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
Wed, 22 Dec 2010 20:08:40 +0100 |
haftmann |
tuned comment
|
file |
diff |
annotate
|
Fri, 17 Dec 2010 20:21:35 +0100 |
wenzelm |
more explicit references to structure Raw_Simplifier;
|
file |
diff |
annotate
|
Fri, 17 Dec 2010 17:08:56 +0100 |
wenzelm |
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
|
file |
diff |
annotate
|
Fri, 17 Dec 2010 14:09:37 +0100 |
wenzelm |
clarified exports of structure Simplifier;
|
file |
diff |
annotate
|
Wed, 25 Aug 2010 18:36:22 +0200 |
wenzelm |
renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
|
file |
diff |
annotate
|
Tue, 15 Jun 2010 14:28:08 +0200 |
haftmann |
tuned whitespace
|
file |
diff |
annotate
|
Mon, 31 May 2010 21:06:57 +0200 |
wenzelm |
modernized some structure names, keeping a few legacy aliases;
|
file |
diff |
annotate
|
Mon, 03 May 2010 14:25:56 +0200 |
wenzelm |
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
|
file |
diff |
annotate
|
Fri, 30 Apr 2010 23:33:42 +0200 |
wenzelm |
export Simplifier.with_context;
|
file |
diff |
annotate
|
Fri, 30 Apr 2010 17:18:29 +0200 |
wenzelm |
conditional warnings: explicitly observe context visibility flag, not just accidental presence of a context;
|
file |
diff |
annotate
|
Thu, 29 Apr 2010 22:56:32 +0200 |
wenzelm |
proper context for mksimps etc. -- via simpset of the running Simplifier;
|
file |
diff |
annotate
|
Sat, 06 Mar 2010 15:39:16 +0100 |
wenzelm |
eliminated Args.bang_facts (legacy feature);
|
file |
diff |
annotate
|
Fri, 19 Feb 2010 16:11:45 +0100 |
wenzelm |
renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;
|
file |
diff |
annotate
|
Fri, 13 Nov 2009 21:11:15 +0100 |
wenzelm |
modernized structure Local_Theory;
|
file |
diff |
annotate
|
Tue, 10 Nov 2009 15:32:43 +0100 |
wenzelm |
define simprocs: do not apply target_morphism prematurely, this is already done in LocalTheory.declaration;
|
file |
diff |
annotate
|
Sun, 08 Nov 2009 16:30:41 +0100 |
wenzelm |
adapted Generic_Data, Proof_Data;
|
file |
diff |
annotate
|
Thu, 05 Nov 2009 22:08:47 +0100 |
wenzelm |
adapted LocalTheory.declaration;
|
file |
diff |
annotate
|
Sun, 25 Oct 2009 19:19:35 +0100 |
wenzelm |
LocalTheory.naming_of;
|
file |
diff |
annotate
|
Sun, 25 Oct 2009 13:04:06 +0100 |
wenzelm |
make SML/NJ happy;
|
file |
diff |
annotate
|
Sat, 24 Oct 2009 20:54:08 +0200 |
wenzelm |
maintain explicit name space kind;
|
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, 24 Oct 2009 19:20:03 +0200 |
wenzelm |
eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;
|
file |
diff |
annotate
|
Wed, 30 Sep 2009 22:25:50 +0200 |
wenzelm |
eliminated dead code;
|
file |
diff |
annotate
|
Tue, 29 Sep 2009 11:49:22 +0200 |
wenzelm |
explicit indication of Unsynchronized.ref;
|
file |
diff |
annotate
|
Thu, 23 Jul 2009 18:44:08 +0200 |
wenzelm |
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
|
file |
diff |
annotate
|
Tue, 21 Jul 2009 01:03:18 +0200 |
wenzelm |
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
|
file |
diff |
annotate
|
Sat, 30 May 2009 12:53:11 +0200 |
wenzelm |
modernized method setup;
|
file |
diff |
annotate
|
Fri, 20 Mar 2009 17:12:37 +0100 |
wenzelm |
Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
|
file |
diff |
annotate
|
Sun, 15 Mar 2009 15:59:44 +0100 |
wenzelm |
simplified attribute setup;
|
file |
diff |
annotate
|
Fri, 13 Mar 2009 21:25:15 +0100 |
wenzelm |
eliminated type Args.T;
|
file |
diff |
annotate
|
Fri, 13 Mar 2009 19:58:26 +0100 |
wenzelm |
unified type Proof.method and pervasive METHOD combinators;
|
file |
diff |
annotate
|
Thu, 12 Mar 2009 11:10:02 +0100 |
wenzelm |
renamed NameSpace.bind to NameSpace.define;
|
file |
diff |
annotate
|
Sun, 08 Mar 2009 12:15:58 +0100 |
wenzelm |
added dest_ss;
|
file |
diff |
annotate
|
Sat, 07 Mar 2009 11:45:56 +0100 |
wenzelm |
renamed rep_ss to MetaSimplifier.internal_ss;
|
file |
diff |
annotate
|
Wed, 21 Jan 2009 23:21:44 +0100 |
wenzelm |
removed Ids;
|
file |
diff |
annotate
|
Fri, 05 Dec 2008 08:04:53 +0100 |
haftmann |
dropped NameSpace.declare_base
|
file |
diff |
annotate
|
Thu, 04 Dec 2008 14:43:33 +0100 |
haftmann |
cleaned up binding module and related code
|
file |
diff |
annotate
|
Thu, 20 Nov 2008 19:06:02 +0100 |
haftmann |
dropped legacy naming code
|
file |
diff |
annotate
|
Fri, 14 Nov 2008 08:50:10 +0100 |
haftmann |
namify and name_decl combinators
|
file |
diff |
annotate
|
Thu, 13 Nov 2008 14:19:09 +0100 |
haftmann |
consider prefixes for name bindings of simprocs (a first approximation)
|
file |
diff |
annotate
|
Tue, 02 Sep 2008 14:10:19 +0200 |
wenzelm |
name/var morphism operates on Name.binding;
|
file |
diff |
annotate
|
Tue, 24 Jun 2008 19:43:14 +0200 |
wenzelm |
ML_Antiquote.value;
|
file |
diff |
annotate
|
Thu, 29 May 2008 23:46:43 +0200 |
wenzelm |
proper context for attribute simplified;
|
file |
diff |
annotate
|
Tue, 15 Apr 2008 16:12:05 +0200 |
wenzelm |
Thm.forall_elim_var(s);
|
file |
diff |
annotate
|
Sat, 29 Mar 2008 22:55:57 +0100 |
wenzelm |
purely functional setup of claset/simpset/clasimpset;
|
file |
diff |
annotate
|
Fri, 28 Mar 2008 20:02:04 +0100 |
wenzelm |
Context.>> : operate on Context.generic;
|
file |
diff |
annotate
|
Thu, 27 Mar 2008 15:32:15 +0100 |
wenzelm |
eliminated delayed theory setup
|
file |
diff |
annotate
|
Thu, 27 Mar 2008 14:41:10 +0100 |
wenzelm |
renamed ML_Context.the_context to ML_Context.the_global_context;
|
file |
diff |
annotate
|
Sat, 01 Sep 2007 15:47:01 +0200 |
wenzelm |
replaced ProofContext.read_term/prop by general Syntax.read_term/prop;
|
file |
diff |
annotate
|
Thu, 02 Aug 2007 12:06:27 +0200 |
wenzelm |
turned simp_depth_limit into configuration option;
|
file |
diff |
annotate
|
Sat, 28 Jul 2007 20:40:30 +0200 |
wenzelm |
added attribute "simproc";
|
file |
diff |
annotate
|
Sun, 08 Jul 2007 19:51:58 +0200 |
wenzelm |
replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
|
file |
diff |
annotate
|
Thu, 05 Jul 2007 20:01:35 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Tue, 03 Jul 2007 17:17:11 +0200 |
wenzelm |
moved (asm_)rewrite_goal_tac from goal.ML to meta_simplifier.ML (no longer depends on SELECT_GOAL);
|
file |
diff |
annotate
|
Thu, 24 May 2007 08:37:37 +0200 |
haftmann |
tuned Pure/General/name_space.ML
|
file |
diff |
annotate
|
Mon, 07 May 2007 00:49:59 +0200 |
wenzelm |
simplified DataFun interfaces;
|
file |
diff |
annotate
|
Mon, 23 Apr 2007 20:44:09 +0200 |
wenzelm |
def_simproc(_i): proper ProofContext.read/cert_terms;
|
file |
diff |
annotate
|
Mon, 16 Apr 2007 16:11:03 +0200 |
haftmann |
canonical merge operations
|
file |
diff |
annotate
|
Sun, 15 Apr 2007 23:25:50 +0200 |
wenzelm |
removed obsolete TypeInfer.logicT -- use dummyT;
|
file |
diff |
annotate
|
Wed, 28 Feb 2007 22:05:44 +0100 |
wenzelm |
exported get_ss, map_ss;
|
file |
diff |
annotate
|
Sun, 04 Feb 2007 22:02:16 +0100 |
wenzelm |
def_simproc(_i): tuned interface;
|
file |
diff |
annotate
|
Mon, 29 Jan 2007 19:58:14 +0100 |
wenzelm |
added get_simproc, @{simproc};
|
file |
diff |
annotate
|
Sun, 28 Jan 2007 23:29:15 +0100 |
wenzelm |
added def_simproc(_i) -- define named simprocs;
|
file |
diff |
annotate
|
Sat, 20 Jan 2007 14:09:17 +0100 |
wenzelm |
added @{simpset};
|
file |
diff |
annotate
|
Fri, 19 Jan 2007 22:08:02 +0100 |
wenzelm |
moved ML context stuff to from Context to ML_Context;
|
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
|
Fri, 10 Nov 2006 07:44:47 +0100 |
haftmann |
introduces canonical AList functions for loop_tacs
|
file |
diff |
annotate
|
Sat, 07 Oct 2006 01:30:58 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Fri, 10 Feb 2006 02:22:16 +0100 |
wenzelm |
Args/Attrib syntax: Context.generic;
|
file |
diff |
annotate
|
Sat, 21 Jan 2006 23:02:14 +0100 |
wenzelm |
simplified type attribute;
|
file |
diff |
annotate
|
Thu, 19 Jan 2006 21:22:08 +0100 |
wenzelm |
setup: theory -> theory;
|
file |
diff |
annotate
|
Sat, 14 Jan 2006 22:25:34 +0100 |
wenzelm |
generic attributes;
|
file |
diff |
annotate
|
Tue, 10 Jan 2006 19:33:27 +0100 |
wenzelm |
Attrib.rule;
|
file |
diff |
annotate
|
Fri, 28 Oct 2005 22:28:02 +0200 |
wenzelm |
export cong_modifiers, simp_modifiers';
|
file |
diff |
annotate
|
Fri, 21 Oct 2005 18:14:47 +0200 |
wenzelm |
added simplification tactics and rules (from meta_simplifier.ML);
|
file |
diff |
annotate
|
Tue, 18 Oct 2005 17:59:31 +0200 |
wenzelm |
renamed set_context to context;
|
file |
diff |
annotate
|
Mon, 17 Oct 2005 23:10:21 +0200 |
wenzelm |
removed obsolete/experimental context components (superceded by Simplifier.the_context);
|
file |
diff |
annotate
|
Thu, 29 Sep 2005 15:50:46 +0200 |
wenzelm |
export debug_bounds;
|
file |
diff |
annotate
|
Tue, 02 Aug 2005 19:47:14 +0200 |
wenzelm |
export clear_ss;
|
file |
diff |
annotate
|
Mon, 01 Aug 2005 19:20:43 +0200 |
wenzelm |
export MataSimplifier.inherit_bounds;
|
file |
diff |
annotate
|
Wed, 13 Jul 2005 16:07:27 +0200 |
wenzelm |
removed obsolete delta stuff;
|
file |
diff |
annotate
|
Wed, 06 Jul 2005 10:41:43 +0200 |
wenzelm |
multiple flags: prefer later ones;
|
file |
diff |
annotate
|
Mon, 04 Jul 2005 20:20:50 +0200 |
wenzelm |
made smlnj happy;
|
file |
diff |
annotate
|
Mon, 04 Jul 2005 20:13:39 +0200 |
wenzelm |
methods: added simp_flags argument, added "depth_limit" flag;
|
file |
diff |
annotate
|
Fri, 17 Jun 2005 18:35:27 +0200 |
wenzelm |
accomodate change of TheoryDataFun;
|
file |
diff |
annotate
|
Sun, 22 May 2005 16:51:03 +0200 |
wenzelm |
moved here from Provers;
|
file |
diff |
annotate
|