| Wed, 21 Feb 2007 13:51:12 +0100 |
krauss |
Fixed print translations for quantifiers a la "ALL x>=t. P x". These used
|
changeset |
files
|
| Wed, 21 Feb 2007 02:30:06 +0100 |
kleing |
prevent quadratic time removal of duplicates if filter list is empty (likely to have too many results)
|
changeset |
files
|
| Tue, 20 Feb 2007 00:53:18 +0100 |
kleing |
added missing \
|
changeset |
files
|
| Tue, 20 Feb 2007 00:23:58 +0100 |
kleing |
updated docs with new with_dups syntax for find_theorems
|
changeset |
files
|
| Tue, 20 Feb 2007 00:14:33 +0100 |
kleing |
Remove duplicates from printed theorems in find_theorems
|
changeset |
files
|
| Mon, 19 Feb 2007 16:44:08 +0100 |
schirmer |
more precise error message in parameter unification
|
changeset |
files
|
| Sat, 17 Feb 2007 18:01:22 +0100 |
aspinall |
Updated
|
changeset |
files
|
| Sat, 17 Feb 2007 18:00:59 +0100 |
aspinall |
Fix <pgipquit>. Remove unused pgmlatomsN. Make showid match askids. Use string functions for showid, avoiding printwrap kludge.
|
changeset |
files
|
| Sat, 17 Feb 2007 17:22:53 +0100 |
aspinall |
<idvalue>: add name attribute to allow unsolicited updates.
|
changeset |
files
|
| Sat, 17 Feb 2007 17:19:59 +0100 |
aspinall |
pretty_full_theory: expose in signature.
|
changeset |
files
|
| Sat, 17 Feb 2007 17:18:47 +0100 |
aspinall |
Clarify comment
|
changeset |
files
|
| Fri, 16 Feb 2007 22:46:03 +0100 |
wenzelm |
unified arity parser/arguments;
|
changeset |
files
|
| Fri, 16 Feb 2007 22:13:16 +0100 |
wenzelm |
ML text: informative Output.debug only;
|
changeset |
files
|
| Fri, 16 Feb 2007 22:13:15 +0100 |
wenzelm |
unified arity parser/arguments;
|
changeset |
files
|
| Fri, 16 Feb 2007 19:19:19 +0100 |
berghofe |
Replaced "raise RecError" by "primrec_err" in function
|
changeset |
files
|
| Fri, 16 Feb 2007 11:01:16 +0100 |
schirmer |
added example for print-mode Axiom
|
changeset |
files
|
| Fri, 16 Feb 2007 11:00:47 +0100 |
schirmer |
added print-mode Axiom to print theorems without premises with a rule on top.
|
changeset |
files
|
| Fri, 16 Feb 2007 09:04:23 +0100 |
krauss |
updated Makefile
|
changeset |
files
|
| Thu, 15 Feb 2007 18:18:21 +0100 |
narboux |
start adding the attribute eqvt to some lemmas of the nominal library
|
changeset |
files
|
| Thu, 15 Feb 2007 17:35:19 +0100 |
krauss |
changed termination goal to use object quantifier
|
changeset |
files
|
| Thu, 15 Feb 2007 12:14:34 +0100 |
krauss |
added congruence rule for function composition
|
changeset |
files
|
| Thu, 15 Feb 2007 12:02:11 +0100 |
krauss |
beta_eta_contract specification befor processing. These normal forms avoid unpleasant surprises later on.
|
changeset |
files
|
| Wed, 14 Feb 2007 10:07:17 +0100 |
haftmann |
continued
|
changeset |
files
|
| Wed, 14 Feb 2007 10:06:17 +0100 |
haftmann |
class package now using Locale.interpretation_i
|
changeset |
files
|
| Wed, 14 Feb 2007 10:06:16 +0100 |
haftmann |
clarified explanation
|
changeset |
files
|
| Wed, 14 Feb 2007 10:06:15 +0100 |
haftmann |
cleanup
|
changeset |
files
|
| Wed, 14 Feb 2007 10:06:14 +0100 |
haftmann |
simpliefied instance statement
|
changeset |
files
|
| Wed, 14 Feb 2007 10:06:13 +0100 |
haftmann |
continued class tutorial
|
changeset |
files
|
| Wed, 14 Feb 2007 10:06:12 +0100 |
haftmann |
added class "preorder"
|
changeset |
files
|
| Tue, 13 Feb 2007 18:26:48 +0100 |
berghofe |
Added nominal_inductive keyword.
|
changeset |
files
|