Mon, 29 Sep 1997 11:37:02 +0200 | paulson | Step_tac -> Safe_tac | changeset | files |
Mon, 29 Sep 1997 11:36:44 +0200 | paulson | Tidied proof of r_comp_rtrancl_eq | changeset | files |
Mon, 29 Sep 1997 11:32:25 +0200 | paulson | qed_spec_mp, normalize_thm, etc. copied in from HOL.ML | changeset | files |