changeset 39941 | 02fcd9cd1eac |
parent 39940 | 1f01c9b2b76b |
child 39950 | f3c4849868b8 |
--- 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.