syntax: renamed 'thmname' to 'thmbind'; added subsection{Antiquotations};

facts: support multiple lists of arguments; method_setup command;

* formal comments (text blocks etc.) in new-style theories may now contain antiquotations of thm/prop/term/typ to be presented according to latex print mode; concrete syntax is like this: @{term[show_types] "f(x) = a + x"}; * Isar: theory command 'method_setup' provides a simple interface for definining proof methods in ML;