wenzelm [Thu, 29 Jun 2000 22:37:24 +0200] rev 9200
syntax: renamed 'thmname' to 'thmbind';
added subsection{Antiquotations};
wenzelm [Thu, 29 Jun 2000 22:36:45 +0200] rev 9199
facts: support multiple lists of arguments;
method_setup command;
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;