# HG changeset patch
# User boehmes
# Date 1260822479 -3600
# Node ID a67bebd37135dbacec97df9b95f6a28be4cb2588
# Parent  c907edcaab36ced3bfedd3305cfadda4bb0c0a7e
replaced blast by metis (blast hangs with polyml-5.2)

diff -r c907edcaab36 -r a67bebd37135 src/HOL/Boogie/Examples/Boogie_Max_Stepwise.thy
--- a/src/HOL/Boogie/Examples/Boogie_Max_Stepwise.thy	Mon Dec 14 11:30:13 2009 +0000
+++ b/src/HOL/Boogie/Examples/Boogie_Max_Stepwise.thy	Mon Dec 14 21:27:59 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