--- 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")
--- 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