src/HOL/ex/Classical.thy

--- a/src/HOL/ex/Classical.thy	Thu Aug 16 21:52:08 2007 +0200
+++ b/src/HOL/ex/Classical.thy	Fri Aug 17 00:03:50 2007 +0200
@@ -430,7 +430,7 @@
 lemma "(\<forall>x y z. R(x,y) & R(y,z) --> R(x,z)) &
        (\<forall>x. \<exists>y. R(x,y)) -->
        ~ (\<forall>x. P x = (\<forall>y. R(x,y) --> ~ P y))"
-by (tactic{*safe_best_meson_tac 1*})
+by (tactic{*Meson.safe_best_meson_tac 1*})
     --{*In contrast, @{text meson} is SLOW: 7.6s on griffon*}
 
 
@@ -724,7 +724,7 @@
        (\<forall>x y. bird x & snail y \<longrightarrow> ~eats x y) &
        (\<forall>x. (caterpillar x \<or> snail x) \<longrightarrow> (\<exists>y. plant y & eats x y))
        \<longrightarrow> (\<exists>x y. animal x & animal y & (\<exists>z. grain z & eats y z & eats x y))"
-by (tactic{*safe_best_meson_tac 1*})
+by (tactic{*Meson.safe_best_meson_tac 1*})
     --{*Nearly twice as fast as @{text meson},
         which performs iterative deepening rather than best-first search*}