Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/UNITY/Comp/AllocBase.thy
changeset 20217 25b068a99d2b
parent 18556 dc39832e9280
child 24147 edc90be09ac1 
--- a/src/HOL/UNITY/Comp/AllocBase.thy	Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/UNITY/Comp/AllocBase.thy	Wed Jul 26 19:23:04 2006 +0200
@@ -35,7 +35,6 @@
       setsum f (lessThan n) <= setsum g (lessThan n)"
 apply (induct_tac "n")
 apply (auto simp add: lessThan_Suc)
-apply (drule_tac x = n in spec, arith)
 done
 
 lemma tokens_mono_prefix [rule_format]:
isabelle