src/HOL/Bali/Basis.thy
changeset 26349 7f5a2f6d9119
parent 24194 96013f81faef
child 27153 56b6cdce22f1
     1.1 --- a/src/HOL/Bali/Basis.thy	Thu Mar 20 12:01:10 2008 +0100
     1.2 +++ b/src/HOL/Bali/Basis.thy	Thu Mar 20 12:01:11 2008 +0100
     1.3 @@ -157,9 +157,7 @@
     1.4  
     1.5  lemma fst_splitE [elim!]: 
     1.6  "[| fst s' = x';  !!x s. [| s' = (x,s);  x = x' |] ==> Q |] ==> Q"
     1.7 -apply (cut_tac p = "s'" in surjective_pairing)
     1.8 -apply auto
     1.9 -done
    1.10 +by (cases s') auto
    1.11  
    1.12  lemma fst_in_set_lemma [rule_format (no_asm)]: "(x, y) : set l --> x : fst ` set l"
    1.13  apply (induct_tac "l")