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 69593 3dda49e08b9d
parent 69064 5840724b1d71
child 70150 cf408ea5f505 
--- a/src/HOL/Library/positivstellensatz.ML	Fri Jan 04 21:49:06 2019 +0100
+++ b/src/HOL/Library/positivstellensatz.ML	Fri Jan 04 23:22:53 2019 +0100
@@ -713,7 +713,7 @@
 
 local
   val absmaxmin_elim_ss1 =
-    simpset_of (put_simpset HOL_basic_ss @{context} addsimps real_abs_thms1)
+    simpset_of (put_simpset HOL_basic_ss \<^context> addsimps real_abs_thms1)
   fun absmaxmin_elim_conv1 ctxt =
     Simplifier.rewrite (put_simpset absmaxmin_elim_ss1 ctxt)
isabelle