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/antisym_setup.ML
changeset 20836 9e40d815e002
parent 19277 f7602e74d948 
--- a/src/HOL/antisym_setup.ML	Mon Oct 02 23:00:51 2006 +0200
+++ b/src/HOL/antisym_setup.ML	Mon Oct 02 23:00:52 2006 +0200
@@ -40,9 +40,9 @@
   end
   handle THM _ => NONE;
 
-val antisym_le = Simplifier.simproc (Theory.sign_of (the_context()))
+val antisym_le = Simplifier.simproc (the_context())
   "antisym le" ["(x::'a::order) <= y"] prove_antisym_le;
-val antisym_less = Simplifier.simproc (Theory.sign_of (the_context()))
+val antisym_less = Simplifier.simproc (the_context())
   "antisym less" ["~ (x::'a::linorder) < y"] prove_antisym_less;
 
 in
isabelle