# HG changeset patch
# User haftmann
# Date 1206010869 -3600
# Node ID 105f552010775255e613fa4f9c39f7c4e3ce359f
# Parent  17debd2fff8e564c825a0f8959758a7a245ac0ad
tuned proofs

diff -r 17debd2fff8e -r 105f55201077 src/HOL/Hilbert_Choice.thy
--- a/src/HOL/Hilbert_Choice.thy	Thu Mar 20 00:20:51 2008 +0100
+++ b/src/HOL/Hilbert_Choice.thy	Thu Mar 20 12:01:09 2008 +0100
@@ -1,5 +1,5 @@
 (*  Title:      HOL/Hilbert_Choice.thy
-    ID: $Id$
+    ID:         $Id$
     Author:     Lawrence C Paulson
     Copyright   2001  University of Cambridge
 *)
@@ -280,13 +280,13 @@
 
 text{*Looping simprule*}
 lemma split_paired_Eps: "(SOME x. P x) = (SOME (a,b). P(a,b))"
-by (simp add: split_Pair_apply)
+  by simp
 
 lemma Eps_split: "Eps (split P) = (SOME xy. P (fst xy) (snd xy))"
-by (simp add: split_def)
+  by (simp add: split_def)
 
 lemma Eps_split_eq [simp]: "(@(x',y'). x = x' & y = y') = (x,y)"
-by blast
+  by blast
 
 
 text{*A relation is wellfounded iff it has no infinite descending chain*}