deleted a step made redundant by the improved rules for setsum
authorpaulson
Tue Jun 20 11:50:33 2000 +0200 (2000-06-20)
changeset 908996dcdd84f1e1
parent 9088 453996655ac2
child 9090 7141b912b0bb
deleted a step made redundant by the improved rules for setsum
src/HOL/Induct/Multiset.ML
     1.1 --- a/src/HOL/Induct/Multiset.ML	Tue Jun 20 11:42:24 2000 +0200
     1.2 +++ b/src/HOL/Induct/Multiset.ML	Tue Jun 20 11:50:33 2000 +0200
     1.3 @@ -332,7 +332,6 @@
     1.4   by (Force_tac 1);
     1.5  by (Clarify_tac 1);
     1.6  by (ftac setsum_SucD 1);
     1.7 - by (assume_tac 1);
     1.8  by (Clarify_tac 1);
     1.9  by (rename_tac "a" 1);
    1.10  by (subgoal_tac "finite{x. 0 < (f(a:=f(a)-1)) x}" 1);