changeset 3427 | e7cef2081106 |
parent 3421 | be777156c7e9 |
child 3842 | b55686a7b22c |
--- a/src/HOL/Univ.ML Fri Jun 06 13:26:41 1997 +0200 +++ b/src/HOL/Univ.ML Fri Jun 06 13:28:40 1997 +0200 @@ -257,7 +257,7 @@ goalw Univ.thy [Scons_def,ntrunc_def] "ntrunc (Suc k) (M$N) = ntrunc k M $ ntrunc k N"; -by (safe_tac (!claset addSIs [equalityI, imageI])); +by (safe_tac (!claset addSIs [imageI])); by (REPEAT (stac ndepth_Push_Node 3 THEN etac Suc_mono 3)); by (REPEAT (rtac Suc_less_SucD 1 THEN rtac (ndepth_Push_Node RS subst) 1 THEN