tuned proof
authorhaftmann
Thu Mar 20 12:01:11 2008 +0100 (2008-03-20)
changeset 263497f5a2f6d9119
parent 26348 0f8e23edd357
child 26350 a170a190c5d3
tuned proof
src/HOL/Bali/Basis.thy
src/HOL/UNITY/ELT.thy
     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")
     2.1 --- a/src/HOL/UNITY/ELT.thy	Thu Mar 20 12:01:10 2008 +0100
     2.2 +++ b/src/HOL/UNITY/ELT.thy	Thu Mar 20 12:01:11 2008 +0100
     2.3 @@ -102,7 +102,8 @@
     2.4  apply (simp (no_asm_use) add: givenBy_eq_Collect)
     2.5  apply safe
     2.6  apply (rule_tac x = "%z. ?R z & ~ ?Q z" in exI)
     2.7 -apply (tactic "deepen_tac (set_cs addSIs [equalityI]) 0 1")
     2.8 +unfolding set_diff_def
     2.9 +apply auto
    2.10  done
    2.11  
    2.12