| Tue, 13 Oct 2015 14:49:15 +0100 | paulson | Fixed nonterminating "blast" proof | changeset | files |
| Tue, 13 Oct 2015 12:42:08 +0100 | paulson | new material on path_component_sets, inside, outside, etc. And more default simprules | changeset | files |
| Tue, 13 Oct 2015 09:21:21 +0200 | haftmann | restored print translation from a1141fb798ff, to prevent a printing misfit observable using "thm divmod_nat_if" in theory "Divides", with a meagure indication in the comment | changeset | files |
| Tue, 13 Oct 2015 09:21:15 +0200 | haftmann | prod_case as canonical name for product type eliminator | changeset | files |