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/Meson/meson_clausify.ML
changeset 42944 9e620869a576
parent 42747 f132d13fcf75
child 43324 2b47822868e4 
--- a/src/HOL/Tools/Meson/meson_clausify.ML	Sun May 22 14:51:41 2011 +0200
+++ b/src/HOL/Tools/Meson/meson_clausify.ML	Sun May 22 14:51:42 2011 +0200
@@ -38,7 +38,7 @@
 
 (* Converts an elim-rule into an equivalent theorem that does not have the
    predicate variable. Leaves other theorems unchanged. We simply instantiate
-   the conclusion variable to False. (Cf. "transform_elim_term" in
+   the conclusion variable to False. (Cf. "transform_elim_prop" in
    "Sledgehammer_Util".) *)
 fun transform_elim_theorem th =
   case concl_of th of    (*conclusion variable*)
isabelle