# HG changeset patch
# User wenzelm
# Date 1305289611 -7200
# Node ID 9984232a0c68368d62678669555756886606e24d
# Parent  dd3ab25eb9d1d8d76e468db8953d1f6e959fbd00
tuned proof;

diff -r dd3ab25eb9d1 -r 9984232a0c68 src/HOL/TLA/TLA.thy
--- a/src/HOL/TLA/TLA.thy	Fri May 13 14:25:35 2011 +0200
+++ b/src/HOL/TLA/TLA.thy	Fri May 13 14:26:51 2011 +0200
@@ -1059,7 +1059,6 @@
   apply (clarsimp simp: leadsto_exists [try_rewrite] not_square [try_rewrite] more_temp_simps)
   apply (erule wf_leadsto)
   apply (rule ensures_simple [temp_use])
-     apply (tactic "TRYALL atac")
    apply (auto simp: square_def angle_def)
   done