# HG changeset patch
# User wenzelm
# Date 1223054257 -7200
# Node ID 7aef230bd145d8b7812f94d8f20bf3490ddd3554
# Parent  8b6af52424f6637ca0a5ef61cce72b69366b6f3b
removed spurious ResAtp.set_prover;

diff -r 8b6af52424f6 -r 7aef230bd145 src/HOL/ex/Primrec.thy
--- 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)