# HG changeset patch
# User wenzelm
# Date 1415457629 -3600
# Node ID a1df119fad45e9caabef0337bf6063877452c8d5
# Parent  97f0ba373b1a9a2c6a14feab5b16e1dec05b0270
updated sledgehammer proof after breakdown of metis (exception Type.TUNIFY);

diff -r 97f0ba373b1a -r a1df119fad45 src/HOL/Metis_Examples/Tarski.thy
--- a/src/HOL/Metis_Examples/Tarski.thy	Sat Nov 08 15:01:05 2014 +0100
+++ b/src/HOL/Metis_Examples/Tarski.thy	Sat Nov 08 15:40:29 2014 +0100
@@ -957,8 +957,7 @@
 
 lemma (in Tarski) f'z_in_int_rel: "[| z \<in> P; \<forall>y\<in>Y. (y, z) \<in> induced P r |]
       ==> ((%x: intY1. f x) z, z) \<in> induced intY1 r"
-apply (metis P_def acc_def fix_imp_eq fix_subset indI reflE restrict_apply subset_eq z_in_interval)
-done
+using P_def fix_imp_eq indI intY1_elem reflE z_in_interval by fastforce
 
 (*never proved, 2007-01-22*)