| Mon, 01 May 2006 18:10:40 +0200 | paulson | some facts about min, max and add, diff | changeset | files |
| 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 |
| Sun, 30 Apr 2006 22:50:06 +0200 | wenzelm | added serial_string; | changeset | files |
| Sun, 30 Apr 2006 22:50:05 +0200 | wenzelm | renamed add_axclass(_i) to define_axclass(_i); | changeset | files |
| Sun, 30 Apr 2006 22:50:03 +0200 | wenzelm | AxClass.axiomatize_arity_i; | changeset | files |
| Sun, 30 Apr 2006 22:50:01 +0200 | wenzelm | AxClass.define_class_i; | changeset | files |
| Sun, 30 Apr 2006 22:49:59 +0200 | wenzelm | * Pure: axclasses now purely definitional; | changeset | files |
| Sat, 29 Apr 2006 23:16:49 +0200 | wenzelm | reduced code duplication; | changeset | files |
| Sat, 29 Apr 2006 23:16:48 +0200 | wenzelm | added insert_list; | changeset | files |
| Sat, 29 Apr 2006 23:16:47 +0200 | wenzelm | added unconstrainT; | changeset | files |
| Sat, 29 Apr 2006 23:16:46 +0200 | wenzelm | added unconstrainTs; | changeset | files |
| Sat, 29 Apr 2006 23:16:45 +0200 | wenzelm | instances data: mutable cache; | changeset | files |
| Sat, 29 Apr 2006 23:16:43 +0200 | wenzelm | tuned; | changeset | files |
| Fri, 28 Apr 2006 17:59:06 +0200 | berghofe | Capitalized theory names. | changeset | files |
| Fri, 28 Apr 2006 17:58:33 +0200 | berghofe | Removed broken proof. | changeset | files |