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
Sun, 27 Nov 2011 23:06:59 +0100
changeset 45653 63ed1be524eb
parent 45652 18214436e1d3
child 45654 cf10bde35973
tuned proof;
src/HOL/HOLCF/FOCUS/Buffer_adm.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/HOLCF/FOCUS/Buffer_adm.thy	Sun Nov 27 22:20:07 2011 +0100
+++ b/src/HOL/HOLCF/FOCUS/Buffer_adm.thy	Sun Nov 27 23:06:59 2011 +0100
@@ -254,7 +254,7 @@
 apply (clarsimp)
 apply (drule (1) fstream_lub_lemma)
 apply (clarsimp)
-apply (tactic "simp_tac (HOL_basic_ss addsimps (ex_simps@all_simps RL[sym])) 1")
+apply (simp only: ex_simps [symmetric] all_simps [symmetric])
 apply (rule_tac x="Xa" in exI)
 apply (rule allI)
 apply (rotate_tac -1)
isabelle