| Sat, 06 Oct 2007 16:50:04 +0200 |
simplified interfaces for outer syntax;
|
file | diff | annotate |
| Mon, 20 Aug 2007 20:43:58 +0200 |
tuned merge operations via pointer_eq;
|
file | diff | annotate |
| Fri, 10 Aug 2007 17:04:24 +0200 |
ClassPackage renamed to Class
|
file | diff | annotate |
| Sat, 28 Jul 2007 20:40:26 +0200 |
added get_cs/map_cs;
|
file | diff | annotate |
| Thu, 05 Jul 2007 20:01:31 +0200 |
renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
|
file | diff | annotate |
| Thu, 31 May 2007 23:47:36 +0200 |
simplified/unified list fold;
|
file | diff | annotate |
| Mon, 07 May 2007 00:49:59 +0200 |
simplified DataFun interfaces;
|
file | diff | annotate |
| Sat, 14 Apr 2007 11:05:12 +0200 |
canonical merge operations
|
file | diff | annotate |
| Tue, 20 Mar 2007 08:27:19 +0100 |
fixed slip
|
file | diff | annotate |
| Mon, 19 Mar 2007 11:59:35 +0100 |
moved Output.overwrite_warn here
|
file | diff | annotate |
| Mon, 26 Feb 2007 23:18:24 +0100 |
moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
|
file | diff | annotate |
| Fri, 19 Jan 2007 22:08:02 +0100 |
moved ML context stuff to from Context to ML_Context;
|
file | diff | annotate |
| Sat, 30 Dec 2006 16:08:03 +0100 |
removed obsolete name_hint handling;
|
file | diff | annotate |
| Thu, 07 Dec 2006 16:46:14 +0100 |
Removal of theorem tagging, which the ATP linkup no longer requires,
|
file | diff | annotate |
| Thu, 07 Dec 2006 00:42:04 +0100 |
reorganized structure Goal vs. Tactic;
|
file | diff | annotate |
| Tue, 05 Dec 2006 00:30:38 +0100 |
thm/prf: separate official name vs. additional tags;
|
file | diff | annotate |
| Fri, 24 Nov 2006 22:05:12 +0100 |
ProofContext.init;
|
file | diff | annotate |
| Wed, 11 Oct 2006 00:27:29 +0200 |
Toplevel: generic_theory;
|
file | diff | annotate |
| Tue, 13 Jun 2006 23:41:41 +0200 |
Drule.equiv_thm supercedes Drule.weak_eq_thm;
|
file | diff | annotate |
| Tue, 14 Mar 2006 16:29:34 +0100 |
ObjectLogic.is_elim;
|
file | diff | annotate |
| Mon, 20 Feb 2006 11:37:18 +0100 |
moved intro_classes from AxClass to ClassPackage
|
file | diff | annotate |
| Fri, 10 Feb 2006 02:22:19 +0100 |
tuned;
|
file | diff | annotate |
| Sun, 29 Jan 2006 19:23:41 +0100 |
default rule step: norm_hhf_tac;
|
file | diff | annotate |
| Sat, 21 Jan 2006 23:02:14 +0100 |
simplified type attribute;
|
file | diff | annotate |
| Thu, 19 Jan 2006 21:22:08 +0100 |
setup: theory -> theory;
|
file | diff | annotate |
| Sun, 15 Jan 2006 19:58:54 +0100 |
attributes: optional weight;
|
file | diff | annotate |
| Sat, 14 Jan 2006 22:25:34 +0100 |
generic attributes;
|
file | diff | annotate |
| Tue, 10 Jan 2006 19:34:04 +0100 |
generic attributes;
|
file | diff | annotate |
| Thu, 05 Jan 2006 22:29:57 +0100 |
store_thm: transfer to current context, i.e. the target theory;
|
file | diff | annotate |
| Wed, 04 Jan 2006 16:14:15 +0100 |
preservation of names
|
file | diff | annotate |
| Tue, 03 Jan 2006 15:44:39 +0100 |
Provers/classical: stricter checks to ensure that supplied intro, dest and
|
file | diff | annotate |
| Sat, 31 Dec 2005 21:49:42 +0100 |
added classical_rule, which replaces Data.make_elim;
|
file | diff | annotate |
| Thu, 08 Dec 2005 20:16:04 +0100 |
swap: no longer pervasive;
|
file | diff | annotate |
| Tue, 22 Nov 2005 19:34:41 +0100 |
Drule.multi_resolves;
|
file | diff | annotate |
| Fri, 28 Oct 2005 17:59:07 +0200 |
Added "deepen" method.
|
file | diff | annotate |
| Mon, 17 Oct 2005 23:10:18 +0200 |
change_claset(_of): more abtract interface;
|
file | diff | annotate |
| Sat, 08 Oct 2005 20:15:34 +0200 |
minor tweaks for Poplog/PML;
|
file | diff | annotate |
| Mon, 05 Sep 2005 08:14:35 +0200 |
introduced binding priority 1 for linear combinators etc.
|
file | diff | annotate |
| Tue, 16 Aug 2005 15:36:28 +0200 |
classical rules must have names for ATP integration
|
file | diff | annotate |
| Tue, 16 Aug 2005 13:42:26 +0200 |
OuterKeyword;
|
file | diff | annotate |
| Wed, 13 Jul 2005 16:07:27 +0200 |
removed obsolete delta stuff;
|
file | diff | annotate |
| Fri, 17 Jun 2005 18:33:05 +0200 |
accomodate change of TheoryDataFun;
|
file | diff | annotate |
| Fri, 15 Apr 2005 12:00:00 +0200 |
Removed most of the atp interface from Pure.
|
file | diff | annotate |
| Wed, 13 Apr 2005 18:45:52 +0200 |
*** MESSAGE REFERS TO PREVIOUS VERSION ***
|
file | diff | annotate |
| Wed, 13 Apr 2005 18:34:22 +0200 |
*** empty log message ***
|
file | diff | annotate |
| Fri, 04 Mar 2005 15:07:34 +0100 |
Removed practically all references to Library.foldr.
|
file | diff | annotate |
| Thu, 03 Mar 2005 12:43:01 +0100 |
Move towards standard functions.
|
file | diff | annotate |
| Sun, 13 Feb 2005 17:15:14 +0100 |
Deleted Library.option type.
|
file | diff | annotate |
| Fri, 21 Jan 2005 18:00:18 +0100 |
Jia Meng: delta simpsets and clasets
|
file | diff | annotate |
| Sun, 11 Jul 2004 20:35:50 +0200 |
context dependent components;
|
file | diff | annotate |
| Fri, 16 Apr 2004 20:59:09 +0200 |
'instance' and intro_classes now handle general sorts;
|
file | diff | annotate |
| Tue, 27 Aug 2002 11:04:00 +0200 |
dup_elim: improved error reporting;
|
file | diff | annotate |
| Tue, 07 May 2002 14:26:32 +0200 |
use eq_thm_prop instead of slightly inadequate eq_thm;
|
file | diff | annotate |
| Thu, 06 Dec 2001 00:41:37 +0100 |
added 'swapped' attribute;
|
file | diff | annotate |
| Wed, 05 Dec 2001 03:12:52 +0100 |
simplified (and clarified) integration with Pure/ContextRules;
|
file | diff | annotate |
| Tue, 04 Dec 2001 18:10:49 +0100 |
made SML/NJ happy;
|
file | diff | annotate |
| Wed, 28 Nov 2001 00:46:26 +0100 |
theory data: removed obsolete finish method;
|
file | diff | annotate |
| Thu, 08 Nov 2001 23:59:37 +0100 |
theory data: finish method;
|
file | diff | annotate |
| Mon, 05 Nov 2001 20:56:29 +0100 |
Method.trace ctxt;
|
file | diff | annotate |
| Mon, 15 Oct 2001 20:36:04 +0200 |
Tactic.orderlist;
|
file | diff | annotate |