wenzelm [Mon, 01 May 2006 17:05:11 +0200] rev 19523
added sort_triv;
wenzelm [Mon, 01 May 2006 17:05:10 +0200] rev 19522
of_sort: simplified derivation;
wenzelm [Mon, 01 May 2006 17:05:09 +0200] rev 19521
adapted arities;
huffman [Mon, 01 May 2006 01:22:31 +0200] rev 19520
add theorem flift2_defined_iff
huffman [Mon, 01 May 2006 01:21:23 +0200] rev 19519
add theorem typdef_flat
wenzelm [Sun, 30 Apr 2006 22:50:12 +0200] rev 19518
AxClass.define_class_i, AxClass.get_definition;
Sign.primitive_arity;
wenzelm [Sun, 30 Apr 2006 22:50:11 +0200] rev 19517
tuned;
wenzelm [Sun, 30 Apr 2006 22:50:10 +0200] rev 19516
AxClass.define_class;
AxClass.axiomatize_class/classrel/arity;
wenzelm [Sun, 30 Apr 2006 22:50:09 +0200] rev 19515
build classes/arities: refer to operations in sorts.ML;
simplified add_class/classrel/arity;
tuned;
wenzelm [Sun, 30 Apr 2006 22:50:08 +0200] rev 19514
moved certify_class/sort to type.ML;
added operations to build sort algebras (from type.ML);
tuned;
wenzelm [Sun, 30 Apr 2006 22:50:07 +0200] rev 19513
removed add_classes/classrel/arities (superceded by AxClass.axiomatize_class/classrel/arity);
added primitive_class/classrel/arity;
wenzelm [Sun, 30 Apr 2006 22:50:06 +0200] rev 19512
added serial_string;
wenzelm [Sun, 30 Apr 2006 22:50:05 +0200] rev 19511
renamed add_axclass(_i) to define_axclass(_i);
renamed get_info to get_definition;
added axiomatize_class/classrel/arity (supercede Sign.add_classes/classrel/arities);
tuned;
wenzelm [Sun, 30 Apr 2006 22:50:03 +0200] rev 19510
AxClass.axiomatize_arity_i;
wenzelm [Sun, 30 Apr 2006 22:50:01 +0200] rev 19509
AxClass.define_class_i;