# HG changeset patch
# User haftmann
# Date 1206010871 -3600
# Node ID 7f5a2f6d9119d126c21a5a1d40c218ee21578180
# Parent  0f8e23edd357ddc1ba2132ab5f809360ea4e45b3
tuned proof

diff -r 0f8e23edd357 -r 7f5a2f6d9119 src/HOL/Bali/Basis.thy
--- a/src/HOL/Bali/Basis.thy	Thu Mar 20 12:01:10 2008 +0100
+++ b/src/HOL/Bali/Basis.thy	Thu Mar 20 12:01:11 2008 +0100
@@ -157,9 +157,7 @@
 
 lemma fst_splitE [elim!]: 
 "[| fst s' = x';  !!x s. [| s' = (x,s);  x = x' |] ==> Q |] ==> Q"
-apply (cut_tac p = "s'" in surjective_pairing)
-apply auto
-done
+by (cases s') auto
 
 lemma fst_in_set_lemma [rule_format (no_asm)]: "(x, y) : set l --> x : fst ` set l"
 apply (induct_tac "l")
diff -r 0f8e23edd357 -r 7f5a2f6d9119 src/HOL/UNITY/ELT.thy
--- a/src/HOL/UNITY/ELT.thy	Thu Mar 20 12:01:10 2008 +0100
+++ b/src/HOL/UNITY/ELT.thy	Thu Mar 20 12:01:11 2008 +0100
@@ -102,7 +102,8 @@
 apply (simp (no_asm_use) add: givenBy_eq_Collect)
 apply safe
 apply (rule_tac x = "%z. ?R z & ~ ?Q z" in exI)
-apply (tactic "deepen_tac (set_cs addSIs [equalityI]) 0 1")
+unfolding set_diff_def
+apply auto
 done