| Wed, 31 Oct 2001 19:37:04 +0100 | berghofe | - enter_thmx -> enter_thms | changeset | files |
| Wed, 31 Oct 2001 19:32:05 +0100 | berghofe | norm_hhf_eq is now stored using open_store_standard_thm. | changeset | files |
| Wed, 31 Oct 2001 01:28:39 +0100 | wenzelm | induct: internalize ``missing'' consumes-facts from goal state | changeset | files |
| Wed, 31 Oct 2001 01:27:04 +0100 | wenzelm | - 'induct' may now use elim-style induction rules without chaining | changeset | files |