Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
merged
authorwenzelm
Tue, 24 Mar 2009 13:20:40 +0100
changeset 30701 9ae91c0d3d1b
parent 30699 08760e217eb7 (diff)
parent 30700 dc38bb27df50 (current diff)
child 30702 274626e2b2dd
child 30707 b0391b9b7103
merged
--- a/src/HOL/Tools/Qelim/presburger.ML	Tue Mar 24 13:12:23 2009 +0100
+++ b/src/HOL/Tools/Qelim/presburger.ML	Tue Mar 24 13:20:40 2009 +0100
@@ -163,8 +163,10 @@
 
 fun cooper_tac elim add_ths del_ths ctxt =
 let val ss = Simplifier.context ctxt (fst (CooperData.get ctxt)) delsimps del_ths addsimps add_ths
+    val aprems = Arith_Data.get_arith_facts ctxt
 in
-  ObjectLogic.full_atomize_tac
+  Method.insert_tac aprems
+  THEN_ALL_NEW ObjectLogic.full_atomize_tac
   THEN_ALL_NEW CONVERSION Thm.eta_long_conversion
   THEN_ALL_NEW simp_tac ss
   THEN_ALL_NEW (TRY o generalize_tac (int_nat_terms ctxt))
isabelle