Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned proof;
authorwenzelm
Fri, 13 May 2011 14:26:51 +0200
changeset 42788 9984232a0c68
parent 42787 dd3ab25eb9d1
child 42789 3a84b6947932
tuned proof;
src/HOL/TLA/TLA.thy file | annotate | diff | comparison | revisions 
--- 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
isabelle