# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1442937239 -3600
# Node ID 1da01148d4b1604eabf610662514300b9d75e2cf
# Parent  e367b93f78e5588c86234c80cd05fbc7f8688c93
Prepared two non-terminating proofs; no obvious link with my changes

diff -r e367b93f78e5 -r 1da01148d4b1 src/HOL/Filter.thy
--- a/src/HOL/Filter.thy	Tue Sep 22 17:13:13 2015 +0200
+++ b/src/HOL/Filter.thy	Tue Sep 22 16:53:59 2015 +0100
@@ -994,7 +994,9 @@
 by(rule le_funI)+(intro fun_mono fun_mono[THEN le_funD, THEN le_funD] order.refl)
 
 lemma rel_filter_conversep [simp]: "rel_filter A\<inverse>\<inverse> = (rel_filter A)\<inverse>\<inverse>"
-by(auto simp add: rel_filter_eventually fun_eq_iff rel_fun_def)
+apply (simp add: rel_filter_eventually fun_eq_iff rel_fun_def)
+apply (safe; metis)
+done
 
 lemma is_filter_parametric_aux:
   assumes "is_filter F"
@@ -1038,7 +1040,8 @@
 apply(rule iffI)
  apply(erule (3) is_filter_parametric_aux)
 apply(erule is_filter_parametric_aux[where A="conversep A"])
-apply(auto simp add: rel_fun_def)
+apply (simp_all add: rel_fun_def)
+apply metis
 done
 
 lemma left_total_rel_filter [transfer_rule]: