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.
fail on merge of conflicting normalization entries: functions are not mergable
authorhaftmann
Thu, 06 May 2010 16:57:59 +0200
changeset 36707 e6933119ea65
parent 36706 b6a47c7d6125
child 36708 3db7243c2484
fail on merge of conflicting normalization entries: functions are not mergable
src/HOL/Tools/Groebner_Basis/normalizer.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Groebner_Basis/normalizer.ML	Thu May 06 16:57:28 2010 +0200
+++ b/src/HOL/Tools/Groebner_Basis/normalizer.ML	Thu May 06 16:57:59 2010 +0200
@@ -55,7 +55,7 @@
   type T = (thm * entry) list;
   val empty = [];
   val extend = I;
-  val merge = AList.merge Thm.eq_thm (K true);
+  val merge = AList.merge Thm.eq_thm (K false);
 );
 
 val get = Data.get o Context.Proof;
isabelle