| Mon, 03 Jul 2006 20:03:11 +0200 |
nipkow |
replaced respects2 by congruent2 because of type problem
|
changeset |
files
|
| Mon, 03 Jul 2006 20:02:42 +0200 |
nipkow |
replaced translation by abbreviation
|
changeset |
files
|
| Mon, 03 Jul 2006 19:33:09 +0200 |
wenzelm |
obtain_export: Thm.generalize;
|
changeset |
files
|
| Mon, 03 Jul 2006 19:33:07 +0200 |
wenzelm |
project_algebra: norm_sort;
|
changeset |
files
|
| Mon, 03 Jul 2006 17:27:09 +0200 |
webertj |
comments fixed, minor optimization wrt. certifying terms
|
changeset |
files
|
| Mon, 03 Jul 2006 17:24:45 +0200 |
dixon |
fix to subst in order to allow subst when head of a term is a bound variable.
|
changeset |
files
|
| Mon, 03 Jul 2006 17:17:41 +0200 |
webertj |
CNF tactic invocations moved into comments
|
changeset |
files
|
| Mon, 03 Jul 2006 16:25:10 +0200 |
webertj |
comment added
|
changeset |
files
|
| Sun, 02 Jul 2006 17:27:10 +0200 |
urbanc |
added more infrastructure for the recursion combinator
|
changeset |
files
|
| Fri, 30 Jun 2006 18:26:36 +0200 |
nipkow |
normal_form to lemma test
|
changeset |
files
|
| Fri, 30 Jun 2006 18:26:22 +0200 |
nipkow |
normalization uses refl now
|
changeset |
files
|
| Fri, 30 Jun 2006 12:22:29 +0200 |
mengj |
Removed some incorrect axioms.
|
changeset |
files
|
| Fri, 30 Jun 2006 12:04:17 +0200 |
haftmann |
fixed stale theory bug
|
changeset |
files
|
| Fri, 30 Jun 2006 12:04:03 +0200 |
haftmann |
slight refinements
|
changeset |
files
|
| Fri, 30 Jun 2006 12:03:36 +0200 |
haftmann |
refinement in instance command
|
changeset |
files
|