# HG changeset patch
# User boehmes
# Date 1260822508 -3600
# Node ID 7f7297f348fe555f840fbe606c40e0c74b9b3387
# Parent  a67bebd37135dbacec97df9b95f6a28be4cb2588# Parent  d6194ece49df94024b792f99821a1b41653977a6
merged

diff -r d6194ece49df -r 7f7297f348fe src/HOL/Boogie/Examples/Boogie_Max_Stepwise.thy
--- a/src/HOL/Boogie/Examples/Boogie_Max_Stepwise.thy	Mon Dec 14 16:35:00 2009 +0100
+++ b/src/HOL/Boogie/Examples/Boogie_Max_Stepwise.thy	Mon Dec 14 21:28:28 2009 +0100
@@ -50,7 +50,7 @@
 text {* Let's find out which assertions of @{text max} are hard to prove: *}
 
 boogie_status (narrow timeout: 4) max
-  (try: (simp add: labels, (fast | blast)?))
+  (try: (simp add: labels, (fast | metis)?))
   -- {* The argument @{text timeout} is optional, restricting the runtime of
         each narrowing step by the given number of seconds. *}
   -- {* The tag @{text try} expects a method to be applied at each narrowing