src/HOL/ex/Classical.thy
changeset 30607 c3d1590debd8
parent 24300 e170cee91c66
child 32262 73cd8f74cf2a
     1.1 --- a/src/HOL/ex/Classical.thy	Fri Mar 20 11:26:59 2009 +0100
     1.2 +++ b/src/HOL/ex/Classical.thy	Fri Mar 20 15:24:18 2009 +0100
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      HOL/ex/Classical
     1.5 -    ID:         $Id$
     1.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7      Copyright   1994  University of Cambridge
     1.8  *)
     1.9 @@ -430,7 +429,7 @@
    1.10  lemma "(\<forall>x y z. R(x,y) & R(y,z) --> R(x,z)) &
    1.11         (\<forall>x. \<exists>y. R(x,y)) -->
    1.12         ~ (\<forall>x. P x = (\<forall>y. R(x,y) --> ~ P y))"
    1.13 -by (tactic{*Meson.safe_best_meson_tac 1*})
    1.14 +by (tactic{*Meson.safe_best_meson_tac @{claset} 1*})
    1.15      --{*In contrast, @{text meson} is SLOW: 7.6s on griffon*}
    1.16  
    1.17  
    1.18 @@ -724,7 +723,7 @@
    1.19         (\<forall>x y. bird x & snail y \<longrightarrow> ~eats x y) &
    1.20         (\<forall>x. (caterpillar x \<or> snail x) \<longrightarrow> (\<exists>y. plant y & eats x y))
    1.21         \<longrightarrow> (\<exists>x y. animal x & animal y & (\<exists>z. grain z & eats y z & eats x y))"
    1.22 -by (tactic{*Meson.safe_best_meson_tac 1*})
    1.23 +by (tactic{*Meson.safe_best_meson_tac @{claset} 1*})
    1.24      --{*Nearly twice as fast as @{text meson},
    1.25          which performs iterative deepening rather than best-first search*}
    1.26