tuned proofs
authorhaftmann
Thu Mar 20 12:01:09 2008 +0100 (2008-03-20)
changeset 26347105f55201077
parent 26346 17debd2fff8e
child 26348 0f8e23edd357
tuned proofs
src/HOL/Hilbert_Choice.thy
     1.1 --- a/src/HOL/Hilbert_Choice.thy	Thu Mar 20 00:20:51 2008 +0100
     1.2 +++ b/src/HOL/Hilbert_Choice.thy	Thu Mar 20 12:01:09 2008 +0100
     1.3 @@ -1,5 +1,5 @@
     1.4  (*  Title:      HOL/Hilbert_Choice.thy
     1.5 -    ID: $Id$
     1.6 +    ID:         $Id$
     1.7      Author:     Lawrence C Paulson
     1.8      Copyright   2001  University of Cambridge
     1.9  *)
    1.10 @@ -280,13 +280,13 @@
    1.11  
    1.12  text{*Looping simprule*}
    1.13  lemma split_paired_Eps: "(SOME x. P x) = (SOME (a,b). P(a,b))"
    1.14 -by (simp add: split_Pair_apply)
    1.15 +  by simp
    1.16  
    1.17  lemma Eps_split: "Eps (split P) = (SOME xy. P (fst xy) (snd xy))"
    1.18 -by (simp add: split_def)
    1.19 +  by (simp add: split_def)
    1.20  
    1.21  lemma Eps_split_eq [simp]: "(@(x',y'). x = x' & y = y') = (x,y)"
    1.22 -by blast
    1.23 +  by blast
    1.24  
    1.25  
    1.26  text{*A relation is wellfounded iff it has no infinite descending chain*}