Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Integ/presburger.ML
changeset 14353 79f9fbef9106
parent 14130 398bc4a885d6
child 14758 af3b71a46a1c 
--- a/src/HOL/Integ/presburger.ML	Mon Jan 12 16:45:35 2004 +0100
+++ b/src/HOL/Integ/presburger.ML	Mon Jan 12 16:51:45 2004 +0100
@@ -184,7 +184,7 @@
       addcongs [conj_le_cong, imp_le_cong]
     (* simp rules for elimination of abs *)
 
-    val simpset3 = HOL_basic_ss addsplits [zabs_split]
+    val simpset3 = HOL_basic_ss addsplits [abs_split]
 	      
     val ct = cterm_of sg (HOLogic.mk_Trueprop t)
isabelle