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/ex/SVC_Oracle.ML
changeset 19277 f7602e74d948
parent 19233 77ca20b0ed77
child 19336 fb5e19d26d5e 
--- a/src/HOL/ex/SVC_Oracle.ML	Thu Mar 16 20:19:25 2006 +0100
+++ b/src/HOL/ex/SVC_Oracle.ML	Fri Mar 17 09:34:23 2006 +0100
@@ -78,8 +78,8 @@
       | fm ((c as Const("True", _))) = c
       | fm ((c as Const("False", _))) = c
       | fm (t as Const("op =",  Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
-      | fm (t as Const("op <",  Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
-      | fm (t as Const("op <=", Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
+      | fm (t as Const("Orderings.less",  Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
+      | fm (t as Const("Orderings.less_eq", Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
       | fm t = replace t
     (*entry point, and abstraction of a meta-formula*)
     fun mt ((c as Const("Trueprop", _)) $ p) = c $ (fm p)
isabelle