src/HOL/ex/cla.ML

 \  (hates agatha agatha & hates agatha charles) & \
 \  (!x. lives(x) & ~richer x agatha --> hates butler x) & \
 \  (!x. hates agatha x --> hates butler x) & \
 \  (!x. ~hates x agatha | ~hates x butler | ~hates x charles) --> \
 \   killed ?who agatha";
-by (Blast_tac 1);
+by (Fast_tac 1);
 result();
 
 writeln"Problem 56";
 goal HOL.thy
     "(! x. (? y. P(y) & x=f(y)) --> P(x)) = (! x. P(x) --> P(f(x)))";