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/Decision_Procs/Approximation.thy
changeset 38864 4abe644fcea5
parent 38786 e46e7a9cb622
child 39556 32a00ff29d1a 
--- a/src/HOL/Decision_Procs/Approximation.thy	Sat Aug 28 20:24:40 2010 +0800
+++ b/src/HOL/Decision_Procs/Approximation.thy	Sat Aug 28 16:14:32 2010 +0200
@@ -3305,7 +3305,7 @@
                              (Const (@{const_name Set.member}, _) $
                               Free (name, _) $ _)) = name
         | variable_of_bound (Const (@{const_name Trueprop}, _) $
-                             (Const (@{const_name "op ="}, _) $
+                             (Const (@{const_name HOL.eq}, _) $
                               Free (name, _) $ _)) = name
         | variable_of_bound t = raise TERM ("variable_of_bound", [t])
isabelle