Mercurial Mercurial > wneuper > isa / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
src/HOL/Tools/Qelim/presburger.ML
changeset 29940 615ac9dc48b1
parent 29885 cdf12a1cb963
parent 29939 126a91027a51
child 29968 bd786c37af84 
     1.1 --- a/src/HOL/Tools/Qelim/presburger.ML	Tue Feb 17 10:52:55 2009 -0800
     1.2 +++ b/src/HOL/Tools/Qelim/presburger.ML	Tue Feb 17 20:42:19 2009 +0000
     1.3 @@ -170,14 +170,14 @@
     1.4    THEN_ALL_NEW simp_tac ss
     1.5    THEN_ALL_NEW (TRY o generalize_tac (int_nat_terms ctxt))
     1.6    THEN_ALL_NEW ObjectLogic.full_atomize_tac
     1.7 -  THEN_ALL_NEW (TRY o thin_prems_tac (is_relevant ctxt))
     1.8 +  THEN_ALL_NEW (thin_prems_tac (is_relevant ctxt))
     1.9    THEN_ALL_NEW ObjectLogic.full_atomize_tac
    1.10    THEN_ALL_NEW div_mod_tac ctxt
    1.11    THEN_ALL_NEW splits_tac ctxt
    1.12    THEN_ALL_NEW simp_tac ss
    1.13    THEN_ALL_NEW CONVERSION Thm.eta_long_conversion
    1.14    THEN_ALL_NEW nat_to_int_tac ctxt
    1.15 -  THEN_ALL_NEW core_cooper_tac ctxt
    1.16 +  THEN_ALL_NEW (core_cooper_tac ctxt)
    1.17    THEN_ALL_NEW finish_tac elim
    1.18  end;
    1.19
wneuper/isa