| Tue, 26 Mar 2019 22:13:36 +0100 | wenzelm | more informative Spec_Rules.Equational, notably primrec argument types; | changeset | files |
| Tue, 26 Mar 2019 14:23:18 +0100 | wenzelm | clarified signature: avoid direct comparison on type rough_classification; | changeset | files |
| Tue, 26 Mar 2019 14:13:03 +0100 | wenzelm | tuned proofs; | changeset | files |
| Tue, 26 Mar 2019 13:45:46 +0100 | wenzelm | removed spurious debugging; | changeset | files |