Prepared two non-terminating proofs; no obvious link with my changes
authorpaulson <lp15@cam.ac.uk>
Tue Sep 22 16:53:59 2015 +0100 (2015-09-22)
changeset 612331da01148d4b1
parent 61230 e367b93f78e5
child 61234 a9e6052188fa
Prepared two non-terminating proofs; no obvious link with my changes
src/HOL/Filter.thy
     1.1 --- a/src/HOL/Filter.thy	Tue Sep 22 17:13:13 2015 +0200
     1.2 +++ b/src/HOL/Filter.thy	Tue Sep 22 16:53:59 2015 +0100
     1.3 @@ -994,7 +994,9 @@
     1.4  by(rule le_funI)+(intro fun_mono fun_mono[THEN le_funD, THEN le_funD] order.refl)
     1.5  
     1.6  lemma rel_filter_conversep [simp]: "rel_filter A\<inverse>\<inverse> = (rel_filter A)\<inverse>\<inverse>"
     1.7 -by(auto simp add: rel_filter_eventually fun_eq_iff rel_fun_def)
     1.8 +apply (simp add: rel_filter_eventually fun_eq_iff rel_fun_def)
     1.9 +apply (safe; metis)
    1.10 +done
    1.11  
    1.12  lemma is_filter_parametric_aux:
    1.13    assumes "is_filter F"
    1.14 @@ -1038,7 +1040,8 @@
    1.15  apply(rule iffI)
    1.16   apply(erule (3) is_filter_parametric_aux)
    1.17  apply(erule is_filter_parametric_aux[where A="conversep A"])
    1.18 -apply(auto simp add: rel_fun_def)
    1.19 +apply (simp_all add: rel_fun_def)
    1.20 +apply metis
    1.21  done
    1.22  
    1.23  lemma left_total_rel_filter [transfer_rule]: