# HG changeset patch
# User wenzelm
# Date 1322431619 -3600
# Node ID 63ed1be524eb6621c82453aefa24debc580d2198
# Parent  18214436e1d39584acffe38d3d05cc53f90ebebc
tuned proof;

diff -r 18214436e1d3 -r 63ed1be524eb src/HOL/HOLCF/FOCUS/Buffer_adm.thy
--- 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)