wenzelm [Thu, 29 Jun 2000 22:35:45 +0200] rev 9198
* 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;
wenzelm [Thu, 29 Jun 2000 22:32:45 +0200] rev 9197
added method_setup;
facts: handle multiple lists of arguments;
wenzelm [Thu, 29 Jun 2000 22:32:08 +0200] rev 9196
facts: handle multiple lists of arguments;
wenzelm [Thu, 29 Jun 2000 22:31:53 +0200] rev 9195
fixed is_semicolon (keyword instead of command!);
wenzelm [Thu, 29 Jun 2000 22:31:29 +0200] rev 9194
added add_method;
wenzelm [Thu, 29 Jun 2000 22:31:12 +0200] rev 9193
have_theorems etc.: handle multiple lists of arguments;
added method_setup;
wenzelm [Thu, 29 Jun 2000 22:29:46 +0200] rev 9192
have_thmss: handle multiple lists of arguments;