--- a/src/HOL/ex/Primrec.thy Fri Oct 03 17:07:41 2008 +0200
+++ b/src/HOL/ex/Primrec.thy Fri Oct 03 19:17:37 2008 +0200
@@ -127,7 +127,6 @@
text {* PROPERTY A 10 *}
-ML{*ResAtp.set_prover "vampire"*}
lemma ack_nest_bound: "ack i1 (ack i2 j) < ack (2 + (i1 + i2)) j"
apply (simp add: numerals)