| Mon, 05 Jul 2010 14:21:30 +0100 |
paulson |
Unification (flexflex) bug fix; making "auto" deterministic
|
file |
diff |
annotate
|
| Mon, 17 May 2010 23:54:15 +0200 |
wenzelm |
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
|
file |
diff |
annotate
|
| Fri, 30 Apr 2010 23:40:14 +0200 |
wenzelm |
map_css: explicitly provide a temporary context, which might be required for mksimps, mkcongs etc.;
|
file |
diff |
annotate
|
| Sat, 06 Mar 2010 15:39:16 +0100 |
wenzelm |
eliminated Args.bang_facts (legacy feature);
|
file |
diff |
annotate
|
| Sun, 01 Nov 2009 15:44:26 +0100 |
wenzelm |
modernized structure Context_Rules;
|
file |
diff |
annotate
|
| Fri, 02 Oct 2009 22:15:08 +0200 |
wenzelm |
eliminated dead code;
|
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
|
| 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 20:25:58 +0100 |
wenzelm |
simplified method setup;
|
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
|
| Sun, 01 Mar 2009 23:36:12 +0100 |
wenzelm |
use long names for old-style fold combinators;
|
file |
diff |
annotate
|
| Sat, 09 Aug 2008 22:43:46 +0200 |
wenzelm |
unified Args.T with OuterLex.token, renamed some operations;
|
file |
diff |
annotate
|
| Sat, 29 Mar 2008 22:55:57 +0100 |
wenzelm |
purely functional setup of claset/simpset/clasimpset;
|
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
|
| Fri, 19 Jan 2007 22:08:02 +0100 |
wenzelm |
moved ML context stuff to from Context to ML_Context;
|
file |
diff |
annotate
|
| Sat, 30 Dec 2006 16:08:03 +0100 |
wenzelm |
removed obsolete name_hint handling;
|
file |
diff |
annotate
|
| Fri, 08 Dec 2006 13:40:26 +0100 |
paulson |
removed use of put_name_hint, as the ATP linkup no longer needs this
|
file |
diff |
annotate
|
| Tue, 05 Dec 2006 00:30:38 +0100 |
wenzelm |
thm/prf: separate official name vs. additional tags;
|
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:29 +0100 |
wenzelm |
generic attributes;
|
file |
diff |
annotate
|
| Sat, 31 Dec 2005 21:49:36 +0100 |
wenzelm |
removed obsolete Provers/make_elim.ML;
|
file |
diff |
annotate
|
| Wed, 21 Dec 2005 12:05:47 +0100 |
paulson |
modified suffix for [iff] attribute
|
file |
diff |
annotate
|
| Mon, 17 Oct 2005 23:10:17 +0200 |
wenzelm |
functor: no Simplifier argument;
|
file |
diff |
annotate
|
| Tue, 16 Aug 2005 15:36:28 +0200 |
paulson |
classical rules must have names for ATP integration
|
file |
diff |
annotate
|
| Sun, 22 May 2005 16:51:07 +0200 |
wenzelm |
Simplifier already setup in Pure;
|
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
|
| Sun, 11 Jul 2004 20:33:22 +0200 |
wenzelm |
local_cla/simpset_of;
|
file |
diff |
annotate
|
| Mon, 21 Jun 2004 10:25:57 +0200 |
kleing |
Merged in license change from Isabelle2004
|
file |
diff |
annotate
|
| Mon, 30 Sep 2002 16:32:05 +0200 |
berghofe |
Introduced addss', which adds asm_lr_simp_tac as a wrapper to the claset.
|
file |
diff |
annotate
|
| Tue, 05 Mar 2002 20:55:20 +0100 |
wenzelm |
iff: conditional rules declared as ``unsafe'';
|
file |
diff |
annotate
|
| Wed, 05 Dec 2001 03:11:05 +0100 |
wenzelm |
iff?: refer to Pure/ContextRules;
|
file |
diff |
annotate
|
| Tue, 23 Oct 2001 19:13:44 +0200 |
wenzelm |
iff: always rotate prems;
|
file |
diff |
annotate
|
| Thu, 09 Aug 2001 19:33:22 +0200 |
oheimb |
corrected semantics of [iff] concerning rules with premises
|
file |
diff |
annotate
|
| Mon, 06 Aug 2001 12:46:21 +0200 |
paulson |
removed the warning from [iff]
|
file |
diff |
annotate
|
| Thu, 31 May 2001 16:52:02 +0200 |
oheimb |
streamlined addIffs/delIffs, added warnings
|
file |
diff |
annotate
|
| Fri, 23 Feb 2001 16:31:21 +0100 |
oheimb |
renamed addaltern to addafter, addSaltern to addSafter
|
file |
diff |
annotate
|
| Sun, 07 Jan 2001 21:41:56 +0100 |
wenzelm |
CHANGED_PROP;
|
file |
diff |
annotate
|
| Tue, 24 Oct 2000 17:35:22 +0200 |
wenzelm |
added clasimpset: unit -> clasimpset;
|
file |
diff |
annotate
|
| Wed, 20 Sep 2000 00:02:26 +0200 |
wenzelm |
made SML/NJ happy;
|
file |
diff |
annotate
|
| Tue, 19 Sep 2000 23:52:37 +0200 |
wenzelm |
added iff_add_global', iff_add_local' (syntax "iff?");
|
file |
diff |
annotate
|
| Wed, 13 Sep 2000 22:31:19 +0200 |
wenzelm |
Args.addN, Args.delN;
|
file |
diff |
annotate
|
| Thu, 07 Sep 2000 20:51:07 +0200 |
wenzelm |
tuned msg;
|
file |
diff |
annotate
|
| Tue, 05 Sep 2000 18:50:12 +0200 |
wenzelm |
added 'iff' declarations;
|
file |
diff |
annotate
|
| Sat, 02 Sep 2000 21:51:14 +0200 |
wenzelm |
added "slowsimp", "bestsimp";
|
file |
diff |
annotate
|
| Fri, 01 Sep 2000 00:31:08 +0200 |
wenzelm |
auto method: opt args;
|
file |
diff |
annotate
|
| Mon, 14 Aug 2000 14:53:26 +0200 |
wenzelm |
added "fastsimp";
|
file |
diff |
annotate
|
| Thu, 03 Aug 2000 00:44:49 +0200 |
wenzelm |
export get_local_clasimpset, clasimp_modifiers;
|
file |
diff |
annotate
|
| Tue, 25 Jul 2000 00:13:11 +0200 |
wenzelm |
added clarsimp method;
|
file |
diff |
annotate
|
| Fri, 21 Jul 2000 17:46:43 +0200 |
oheimb |
strengthened force_tac by using new first_best_tac
|
file |
diff |
annotate
|
| Fri, 31 Mar 2000 21:58:34 +0200 |
wenzelm |
added change_global/local_css;
|
file |
diff |
annotate
|
| Wed, 15 Mar 2000 18:40:03 +0100 |
wenzelm |
include Splitter.split_modifiers;
|
file |
diff |
annotate
|
| Fri, 28 Jan 2000 21:57:15 +0100 |
wenzelm |
HEADGOAL;
|
file |
diff |
annotate
|
| Fri, 28 Jan 2000 12:12:06 +0100 |
wenzelm |
replaced FIRSTGOAL by FINDGOAL (backtracking!);
|
file |
diff |
annotate
|
| Wed, 27 Oct 1999 19:29:47 +0200 |
oheimb |
clarsimp_tac now copes with the (unwanted) case that the simplifier splits
|
file |
diff |
annotate
|
| Tue, 21 Sep 1999 17:26:50 +0200 |
wenzelm |
setup for refined facts handling;
|
file |
diff |
annotate
|