# HG changeset patch
# User wenzelm
# Date 1415457881 -3600
# Node ID cdf46ae368b412cd9beb775351a3f4dd99214b55
# Parent  a1df119fad45e9caabef0337bf6063877452c8d5
updated some sledgehammer proofs -- much faster;

diff -r a1df119fad45 -r cdf46ae368b4 src/HOL/Metis_Examples/Tarski.thy
--- a/src/HOL/Metis_Examples/Tarski.thy	Sat Nov 08 15:40:29 2014 +0100
+++ b/src/HOL/Metis_Examples/Tarski.thy	Sat Nov 08 15:44:41 2014 +0100
@@ -567,10 +567,11 @@
 apply (rule sym)
 apply (simp add: P_def)
 apply (rule lubI)
-apply (metis P_def fix_subset)
-apply (metis Collect_conj_eq Collect_mem_eq Int_commute Int_lower1 lub_in_lattice vimage_def)
-apply (metis P_def fixf_le_lubH)
-by (metis P_def lubH_least_fixf)
+apply (simp add: fix_subset)
+using fix_subset lubH_is_fixp apply fastforce
+apply (simp add: fixf_le_lubH)
+using lubH_is_fixp apply blast
+done
 
 declare CL.lubI[rule del] fix_subset[rule del] CL.lub_in_lattice[rule del]
         CLF.fixf_le_lubH[simp del] CLF.lubH_least_fixf[simp del]