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/Library/positivstellensatz.ML
changeset 36700 9b85b9d74b83
parent 35408 b48ab741683b
child 36721 bfd7f5c3bf69 
--- a/src/HOL/Library/positivstellensatz.ML	Wed May 05 16:53:21 2010 +0200
+++ b/src/HOL/Library/positivstellensatz.ML	Thu May 06 16:32:20 2010 +0200
@@ -748,7 +748,7 @@
   fun simple_cterm_ord t u = Term_Ord.term_ord (term_of t, term_of u) = LESS
   val {add,mul,neg,pow,sub,main} = 
      Normalizer.semiring_normalizers_ord_wrapper ctxt
-      (the (NormalizerData.match ctxt @{cterm "(0::real) + 1"})) 
+      (the (Normalizer.match ctxt @{cterm "(0::real) + 1"})) 
      simple_cterm_ord
 in gen_real_arith ctxt
    (cterm_of_rat, field_comp_conv, field_comp_conv,field_comp_conv,
isabelle