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/Tools/Function/termination.ML
changeset 47433 07f4bf913230
parent 46218 ecf6375e2abb
child 47835 2d48bf79b725 
--- a/src/HOL/Tools/Function/termination.ML	Tue Apr 03 08:55:06 2012 +0200
+++ b/src/HOL/Tools/Function/termination.ML	Tue Apr 03 17:26:30 2012 +0900
@@ -141,7 +141,7 @@
 fun prove_chain thy chain_tac (c1, c2) =
   let
     val goal =
-      HOLogic.mk_eq (HOLogic.mk_binop @{const_name Relation.rel_comp} (c1, c2),
+      HOLogic.mk_eq (HOLogic.mk_binop @{const_name Relation.relcomp} (c1, c2),
         Const (@{const_abbrev Set.empty}, fastype_of c1))
       |> HOLogic.mk_Trueprop (* "C1 O C2 = {}" *)
   in
isabelle