| Mon, 01 May 2006 18:10:18 +0200 |
paulson |
a few more examples
|
changeset |
files
|
| Mon, 01 May 2006 17:05:13 +0200 |
wenzelm |
class_triv: Sign.certify_class;
|
changeset |
files
|
| Mon, 01 May 2006 17:05:12 +0200 |
wenzelm |
arities: maintain original codomain;
|
changeset |
files
|
| Mon, 01 May 2006 17:05:11 +0200 |
wenzelm |
added sort_triv;
|
changeset |
files
|
| Mon, 01 May 2006 17:05:10 +0200 |
wenzelm |
of_sort: simplified derivation;
|
changeset |
files
|
| Mon, 01 May 2006 17:05:09 +0200 |
wenzelm |
adapted arities;
|
changeset |
files
|
| Mon, 01 May 2006 01:22:31 +0200 |
huffman |
add theorem flift2_defined_iff
|
changeset |
files
|
| Mon, 01 May 2006 01:21:23 +0200 |
huffman |
add theorem typdef_flat
|
changeset |
files
|
| Sun, 30 Apr 2006 22:50:12 +0200 |
wenzelm |
AxClass.define_class_i, AxClass.get_definition;
|
changeset |
files
|
| Sun, 30 Apr 2006 22:50:11 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 30 Apr 2006 22:50:10 +0200 |
wenzelm |
AxClass.define_class;
|
changeset |
files
|
| Sun, 30 Apr 2006 22:50:09 +0200 |
wenzelm |
build classes/arities: refer to operations in sorts.ML;
|
changeset |
files
|
| Sun, 30 Apr 2006 22:50:08 +0200 |
wenzelm |
moved certify_class/sort to type.ML;
|
changeset |
files
|
| Sun, 30 Apr 2006 22:50:07 +0200 |
wenzelm |
removed add_classes/classrel/arities (superceded by AxClass.axiomatize_class/classrel/arity);
|
changeset |
files
|