# HG changeset patch # User wenzelm # Date 898784921 -7200 # Node ID ee8a754f198187fba03b1bf4a965826c1b247b11 # Parent ef479934678be226948c9adef52feafc1db08597 fixed unit_eq; diff -r ef479934678b -r ee8a754f1981 src/HOLCF/One.ML --- a/src/HOLCF/One.ML Thu Jun 25 16:13:20 1998 +0200 +++ b/src/HOLCF/One.ML Thu Jun 25 16:28:41 1998 +0200 @@ -16,9 +16,8 @@ (fn prems => [ (lift.induct_tac "t" 1), - (fast_tac HOL_cs 1), (Simp_tac 1), - (rtac unit_eq 1) + (Simp_tac 1) ]); qed_goal "oneE" thy