diff -r 1f01c9b2b76b -r 02fcd9cd1eac src/HOL/Tools/Meson/meson.ML --- a/src/HOL/Tools/Meson/meson.ML Mon Oct 04 21:37:42 2010 +0200 +++ b/src/HOL/Tools/Meson/meson.ML Mon Oct 04 21:49:07 2010 +0200 @@ -1,5 +1,6 @@ -(* Title: HOL/Tools/meson.ML +(* Title: HOL/Tools/Meson/meson.ML Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Author: Jasmin Blanchette, TU Muenchen The MESON resolution proof procedure for HOL. When making clauses, avoids using the rewriter -- instead uses RS recursively.