| Wed, 07 Feb 2007 17:28:09 +0100 |
berghofe |
Adapted to new inductive definition package.
|
changeset |
files
|
| Wed, 07 Feb 2007 17:26:49 +0100 |
berghofe |
Adapted to changes in Transitive_Closure theory.
|
changeset |
files
|
| Wed, 07 Feb 2007 17:26:04 +0100 |
berghofe |
Added Predicate theory.
|
changeset |
files
|
| Wed, 07 Feb 2007 17:25:39 +0100 |
berghofe |
New theory for converting between predicates and sets.
|
changeset |
files
|
| Wed, 07 Feb 2007 13:05:28 +0100 |
bulwahn |
changes in lexicographic_order termination tactic
|
changeset |
files
|
| Wed, 07 Feb 2007 12:08:48 +0100 |
berghofe |
"prove" function now instantiates relation variable in order
|
changeset |
files
|
| Wed, 07 Feb 2007 12:05:54 +0100 |
berghofe |
Made untabify function tail recursive.
|
changeset |
files
|
| Tue, 06 Feb 2007 19:32:32 +0100 |
wenzelm |
tuned matches_subterm;
|
changeset |
files
|
| Tue, 06 Feb 2007 19:32:31 +0100 |
wenzelm |
trace/debug: avoid eager string concatenation;
|
changeset |
files
|
| Tue, 06 Feb 2007 18:02:28 +0100 |
wenzelm |
cc: removed option -lstdc++, which seems to be unnecessry, but causes problems on some platforms;
|
changeset |
files
|
| Tue, 06 Feb 2007 17:20:14 +0100 |
wenzelm |
pervasive exception Option;
|
changeset |
files
|
| Tue, 06 Feb 2007 17:06:44 +0100 |
wenzelm |
added has_kind/get_kind;
|
changeset |
files
|
| Tue, 06 Feb 2007 15:12:18 +0100 |
urbanc |
fixed two stupid bugs of SML to do with the value restriction and missing type
|
changeset |
files
|
| Tue, 06 Feb 2007 12:54:55 +0100 |
aspinall |
askids/qualified_thms_of_thy: version which returns names in domain of get_thm
|
changeset |
files
|