| Wed, 04 Mar 2009 11:44:05 +0100 | haftmann | consequent rewrite of index_size, size [index] to nat_of; support pseudo-primrec sepcifications with fun | changeset | files |
| Wed, 04 Mar 2009 11:37:50 +0100 | haftmann | merged | changeset | files |
| Wed, 04 Mar 2009 10:52:47 +0100 | haftmann | explicit error message for `improper` instances lacking explicit instance parameter constants | changeset | files |
| Wed, 04 Mar 2009 11:05:29 +0100 | blanchet | Merge. | changeset | files |
| Wed, 04 Mar 2009 11:05:02 +0100 | blanchet | Merge. | changeset | files |
| Wed, 04 Mar 2009 10:45:52 +0100 | blanchet | Merge. | changeset | files |
| Wed, 04 Mar 2009 10:43:39 +0100 | blanchet | Made Refute.norm_rhs public, so I can use it in Nitpick. | changeset | files |
| Sun, 01 Mar 2009 18:40:16 +0100 | blanchet | Added "nitpick_const_def" attribute, for overriding the definition axiom of a constant. | changeset | files |