Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
deleted a step made redundant by the improved rules for setsum
authorpaulson
Tue, 20 Jun 2000 11:50:33 +0200 (2000-06-20)
changeset 9089 96dcdd84f1e1
parent 9088 453996655ac2
child 9090 7141b912b0bb
deleted a step made redundant by the improved rules for setsum
src/HOL/Induct/Multiset.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Induct/Multiset.ML	Tue Jun 20 11:42:24 2000 +0200
+++ b/src/HOL/Induct/Multiset.ML	Tue Jun 20 11:50:33 2000 +0200
@@ -332,7 +332,6 @@
  by (Force_tac 1);
 by (Clarify_tac 1);
 by (ftac setsum_SucD 1);
- by (assume_tac 1);
 by (Clarify_tac 1);
 by (rename_tac "a" 1);
 by (subgoal_tac "finite{x. 0 < (f(a:=f(a)-1)) x}" 1);
isabelle