1.1 --- a/src/HOL/Metis_Examples/Tarski.thy	Tue Mar 20 10:06:35 2012 +0100
     1.2 +++ b/src/HOL/Metis_Examples/Tarski.thy	Tue Mar 20 10:21:05 2012 +0100
     1.3 @@ -487,13 +487,7 @@
     1.4  apply (rule lub_upper, fast)
     1.5  apply (rule_tac t = "H" in ssubst, assumption)
     1.6  apply (rule CollectI)
     1.7 -apply (rule conjI)
     1.8 -(*??no longer terminates, with combinators
     1.9 -apply (metis CO_refl_on lubH_le_flubH monotone_def monotone_f reflD1 reflD2)
    1.10 -*)
    1.11 -apply (metis CO_refl_on lubH_le_flubH monotoneE [OF monotone_f] refl_onD1 refl_onD2)
    1.12 -apply (metis CO_refl_on lubH_le_flubH refl_onD2)
    1.13 -done
    1.14 +by (metis (lifting) CO_refl_on lubH_le_flubH monotone_def monotone_f refl_onD1 refl_onD2)
    1.15  
    1.16  declare CLF.f_in_funcset[rule del] funcset_mem[rule del]
    1.17          CL.lub_in_lattice[rule del] PO.monotoneE[rule del]
    1.18 @@ -575,13 +569,8 @@
    1.19  apply (rule lubI)
    1.20  apply (metis P_def fix_subset)
    1.21  apply (metis Collect_conj_eq Collect_mem_eq Int_commute Int_lower1 lub_in_lattice vimage_def)
    1.22 -(*??no longer terminates, with combinators
    1.23 -apply (metis P_def fix_def fixf_le_lubH)
    1.24 -apply (metis P_def fix_def lubH_least_fixf)
    1.25 -*)
    1.26 -apply (simp add: fixf_le_lubH)
    1.27 -apply (simp add: lubH_least_fixf)
    1.28 -done
    1.29 +apply (metis P_def fixf_le_lubH)
    1.30 +by (metis P_def lubH_least_fixf)
    1.31  
    1.32  declare CL.lubI[rule del] fix_subset[rule del] CL.lub_in_lattice[rule del]
    1.33          CLF.fixf_le_lubH[simp del] CLF.lubH_least_fixf[simp del]