changeset 41144 | 509e51b7509a |
parent 41141 | ad923cdd4a5d |
child 41413 | 64cd30d6b0b8 |
--- a/src/HOL/Metis_Examples/Tarski.thy Wed Dec 15 11:26:28 2010 +0100 +++ b/src/HOL/Metis_Examples/Tarski.thy Wed Dec 15 11:26:28 2010 +0100 @@ -1,7 +1,8 @@ (* Title: HOL/Metis_Examples/Tarski.thy Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Author: Jasmin Blanchette, TU Muenchen -Testing the metis method. +Testing Metis. *) header {* The Full Theorem of Tarski *}