src/HOL/TLA/TLA.thy
changeset 42788 9984232a0c68
parent 42787 dd3ab25eb9d1
child 42793 88bee9f6eec7
     1.1 --- a/src/HOL/TLA/TLA.thy	Fri May 13 14:25:35 2011 +0200
     1.2 +++ b/src/HOL/TLA/TLA.thy	Fri May 13 14:26:51 2011 +0200
     1.3 @@ -1059,7 +1059,6 @@
     1.4    apply (clarsimp simp: leadsto_exists [try_rewrite] not_square [try_rewrite] more_temp_simps)
     1.5    apply (erule wf_leadsto)
     1.6    apply (rule ensures_simple [temp_use])
     1.7 -     apply (tactic "TRYALL atac")
     1.8     apply (auto simp: square_def angle_def)
     1.9    done
    1.10