| Thu, 21 Apr 2005 18:57:18 +0200 |
berghofe |
Adapted to new interface of instantiation and unification / matching functions.
|
file |
diff |
annotate
|
| Wed, 13 Apr 2005 18:46:04 +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
|
| Mon, 11 Oct 2004 07:39:19 +0200 |
nipkow |
Induction now preserves the name of the induction variable.
|
file |
diff |
annotate
|
| Mon, 21 Jun 2004 10:25:57 +0200 |
kleing |
Merged in license change from Isabelle2004
|
file |
diff |
annotate
|
| Sat, 21 Feb 2004 08:43:08 +0100 |
nipkow |
Transitive_Closure: added consumes and case_names attributes
|
file |
diff |
annotate
|
| Mon, 30 Sep 2002 15:45:11 +0200 |
nipkow |
fixes !!-bound vars in induction statement automatically
|
file |
diff |
annotate
|
| Fri, 26 Jul 2002 21:09:39 +0200 |
wenzelm |
support for split assumptions in cases (hyps vs. prems);
|
file |
diff |
annotate
|
| Fri, 31 May 2002 18:49:31 +0200 |
berghofe |
Changed interface of MetaSimplifier.rewrite_term.
|
file |
diff |
annotate
|
| Tue, 07 May 2002 14:26:32 +0200 |
wenzelm |
use eq_thm_prop instead of slightly inadequate eq_thm;
|
file |
diff |
annotate
|
| Sat, 26 Jan 2002 19:17:15 +0100 |
wenzelm |
cases: really append cases_default;
|
file |
diff |
annotate
|
| Thu, 17 Jan 2002 21:02:18 +0100 |
wenzelm |
MetaSimplifier.rewrite_term replaces slow Tactic.rewrite_cterm;
|
file |
diff |
annotate
|