| Tue, 13 Jun 2006 23:41:41 +0200 |
wenzelm |
Drule.equiv_thm supercedes Drule.weak_eq_thm;
|
file |
diff |
annotate
|
| Tue, 14 Mar 2006 16:29:34 +0100 |
wenzelm |
ObjectLogic.is_elim;
|
file |
diff |
annotate
|
| Mon, 20 Feb 2006 11:37:18 +0100 |
haftmann |
moved intro_classes from AxClass to ClassPackage
|
file |
diff |
annotate
|
| Fri, 10 Feb 2006 02:22:19 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 29 Jan 2006 19:23:41 +0100 |
wenzelm |
default rule step: norm_hhf_tac;
|
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
|
| Sun, 15 Jan 2006 19:58:54 +0100 |
wenzelm |
attributes: optional weight;
|
file |
diff |
annotate
|
| Sat, 14 Jan 2006 22:25:34 +0100 |
wenzelm |
generic attributes;
|
file |
diff |
annotate
|
| Tue, 10 Jan 2006 19:34:04 +0100 |
wenzelm |
generic attributes;
|
file |
diff |
annotate
|
| Thu, 05 Jan 2006 22:29:57 +0100 |
wenzelm |
store_thm: transfer to current context, i.e. the target theory;
|
file |
diff |
annotate
|
| Wed, 04 Jan 2006 16:14:15 +0100 |
paulson |
preservation of names
|
file |
diff |
annotate
|
| Tue, 03 Jan 2006 15:44:39 +0100 |
paulson |
Provers/classical: stricter checks to ensure that supplied intro, dest and
|
file |
diff |
annotate
|
| Sat, 31 Dec 2005 21:49:42 +0100 |
wenzelm |
added classical_rule, which replaces Data.make_elim;
|
file |
diff |
annotate
|
| Thu, 08 Dec 2005 20:16:04 +0100 |
wenzelm |
swap: no longer pervasive;
|
file |
diff |
annotate
|
| Tue, 22 Nov 2005 19:34:41 +0100 |
wenzelm |
Drule.multi_resolves;
|
file |
diff |
annotate
|
| Fri, 28 Oct 2005 17:59:07 +0200 |
berghofe |
Added "deepen" method.
|
file |
diff |
annotate
|
| Mon, 17 Oct 2005 23:10:18 +0200 |
wenzelm |
change_claset(_of): more abtract interface;
|
file |
diff |
annotate
|
| Sat, 08 Oct 2005 20:15:34 +0200 |
wenzelm |
minor tweaks for Poplog/PML;
|
file |
diff |
annotate
|
| Mon, 05 Sep 2005 08:14:35 +0200 |
haftmann |
introduced binding priority 1 for linear combinators etc.
|
file |
diff |
annotate
|
| Tue, 16 Aug 2005 15:36:28 +0200 |
paulson |
classical rules must have names for ATP integration
|
file |
diff |
annotate
|
| Tue, 16 Aug 2005 13:42:26 +0200 |
wenzelm |
OuterKeyword;
|
file |
diff |
annotate
|
| Wed, 13 Jul 2005 16:07:27 +0200 |
wenzelm |
removed obsolete delta stuff;
|
file |
diff |
annotate
|
| Fri, 17 Jun 2005 18:33:05 +0200 |
wenzelm |
accomodate change of TheoryDataFun;
|
file |
diff |
annotate
|
| Fri, 15 Apr 2005 12:00:00 +0200 |
ballarin |
Removed most of the atp interface from Pure.
|
file |
diff |
annotate
|
| Wed, 13 Apr 2005 18:45:52 +0200 |
wenzelm |
*** MESSAGE REFERS TO PREVIOUS VERSION ***
|
file |
diff |
annotate
|
| Wed, 13 Apr 2005 18:34:22 +0200 |
wenzelm |
*** empty log message ***
|
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
|