Thu, 20 Nov 1997 11:55:39 +0100 | paulson | Now uses induct_tac | changeset | files |
Thu, 20 Nov 1997 11:54:31 +0100 | paulson | Updated the NatSum example | changeset | files |
Thu, 20 Nov 1997 11:53:51 +0100 | paulson | New, higher-level definition of \\out macro | changeset | files |
Thu, 20 Nov 1997 11:03:53 +0100 | paulson | Speeded up the proof of succ_lt_induct_lemma | changeset | files |
Thu, 20 Nov 1997 11:03:26 +0100 | paulson | Two new rewrites | changeset | files |
Thu, 20 Nov 1997 10:55:27 +0100 | paulson | Got rid of some slow deepen_tac calls | changeset | files |
Thu, 20 Nov 1997 10:54:04 +0100 | paulson | Renamed "overload" to "overloaded" for sml/nj compatibility | changeset | files |
Thu, 20 Nov 1997 10:50:51 +0100 | paulson | No more makeatletter/other | changeset | files |