| Wed, 18 Jun 2008 18:54:57 +0200 |
wenzelm |
simplified Abel_Cancel setup;
|
file |
diff |
annotate
|
| Sat, 15 Sep 2007 19:27:35 +0200 |
haftmann |
fixed title
|
file |
diff |
annotate
|
| Thu, 17 May 2007 19:49:40 +0200 |
haftmann |
canonical prefixing of class constants
|
file |
diff |
annotate
|
| Tue, 26 Sep 2006 13:34:16 +0200 |
haftmann |
renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
|
file |
diff |
annotate
|
| Sat, 08 Jul 2006 12:54:43 +0200 |
wenzelm |
simprocs: no theory argument -- use simpset context instead;
|
file |
diff |
annotate
|
| Tue, 06 Jun 2006 20:42:28 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 10 Mar 2006 15:33:48 +0100 |
haftmann |
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
|
file |
diff |
annotate
|
| Fri, 21 Oct 2005 18:14:34 +0200 |
wenzelm |
Goal.prove;
|
file |
diff |
annotate
|
| Mon, 17 Oct 2005 23:10:15 +0200 |
wenzelm |
Simplifier.inherit_context instead of Simplifier.inherit_bounds;
|
file |
diff |
annotate
|
| Mon, 01 Aug 2005 19:20:26 +0200 |
wenzelm |
simprocs: Simplifier.inherit_bounds;
|
file |
diff |
annotate
|
| Sat, 25 Jun 2005 16:07:13 +0200 |
nipkow |
cancels completely within terms as well now.
|
file |
diff |
annotate
|
| Fri, 17 Jun 2005 18:33:03 +0200 |
wenzelm |
renamed sg_ref to thy_ref;
|
file |
diff |
annotate
|
| Thu, 21 Apr 2005 19:02:54 +0200 |
berghofe |
Moved cterm_fun from Thm to Drule.
|
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, 06 Sep 2004 16:45:10 +0200 |
paulson |
now rejects degenerate (looping) cases
|
file |
diff |
annotate
|
| Tue, 03 Aug 2004 14:48:59 +0200 |
ballarin |
Typo.
|
file |
diff |
annotate
|
| Thu, 08 Jul 2004 19:34:56 +0200 |
wenzelm |
adapted type of simprocs;
|
file |
diff |
annotate
|
| Tue, 18 May 2004 11:45:50 +0200 |
obua |
modified abel_cancel.ML for polymorphic types
|
file |
diff |
annotate
|
| Thu, 08 Aug 2002 23:46:09 +0200 |
wenzelm |
use Tactic.prove instead of prove_goalw_cterm in internal proofs!
|
file |
diff |
annotate
|
| Tue, 06 Aug 2002 11:22:05 +0200 |
wenzelm |
sane interface for simprocs;
|
file |
diff |
annotate
|
| Wed, 21 Nov 2001 00:36:51 +0100 |
wenzelm |
use tracing function for trace output;
|
file |
diff |
annotate
|
| Mon, 24 Jul 2000 23:47:57 +0200 |
wenzelm |
do not pass theory values, but sg_ref;
|
file |
diff |
annotate
|
| Tue, 30 May 2000 16:03:09 +0200 |
wenzelm |
global timing flag;
|
file |
diff |
annotate
|
| Thu, 23 Sep 1999 13:09:39 +0200 |
paulson |
The restrict_to_left rule fixes some bugs
|
file |
diff |
annotate
|
| Wed, 17 Mar 1999 16:33:47 +0100 |
wenzelm |
Theory.sign_of;
|
file |
diff |
annotate
|
| Thu, 22 Oct 1998 12:35:40 +0200 |
wenzelm |
eliminated 'let ... in structure ...' to make SML/NJ 0.93 happy;
|
file |
diff |
annotate
|
| Mon, 05 Oct 1998 10:19:21 +0200 |
paulson |
simpler interface for Abel_Cancel
|
file |
diff |
annotate
|
| Thu, 01 Oct 1998 18:19:34 +0200 |
paulson |
new simproc functor
|
file |
diff |
annotate
|