2000-09-01 wenzelm 2000-09-01 'declare' made proper command;
2000-09-01 wenzelm 2000-09-01 priority_fn := decorate_lines; replaced 'message' by 'priority';
2000-09-01 wenzelm 2000-09-01 added priority, priority_fn;
2000-09-01 wenzelm 2000-09-01 added "safe" method;
2000-09-01 wenzelm 2000-09-01 auto method: opt args; tuned;
2000-09-01 wenzelm 2000-09-01 converted Lambda scripts;
2000-09-01 wenzelm 2000-09-01 converted;
2000-09-01 wenzelm 2000-09-01 fixed rulify_prems;
2000-09-01 wenzelm 2000-09-01 lemmas [mono] = lists_mono;
2000-09-01 wenzelm 2000-09-01 updated;
2000-08-31 wenzelm 2000-08-31 fixed make_pp; basic interrupt handling;
2000-08-31 wenzelm 2000-08-31 improved exit function for polyml-4.0;
2000-08-31 kleing 2000-08-31 tuned
2000-08-31 nipkow 2000-08-31 *** empty log message ***
2000-08-31 wenzelm 2000-08-31 ported HOL/Lambda/ListBeta;
2000-08-31 wenzelm 2000-08-31 improved handling of messages: do not decorate writeln output;
2000-08-31 wenzelm 2000-08-31 improved messages;
2000-08-31 wenzelm 2000-08-31 more polyml choices; tuned;
2000-08-30 kleing 2000-08-30 added some bind_thm
2000-08-30 kleing 2000-08-30 functional LBV style, dead code, type safety -> Isar
2000-08-30 kleing 2000-08-30 MicroJava changed (all of BV -> Isar)
2000-08-30 kleing 2000-08-30 tuned
2000-08-30 nipkow 2000-08-30 *** empty log message ***
2000-08-30 wenzelm 2000-08-30 tuned;
2000-08-30 wenzelm 2000-08-30 renamed antiquotation 'name' to 'text'; added antiquotation option 'source';
2000-08-30 wenzelm 2000-08-30 tuned;
2000-08-30 wenzelm 2000-08-30 added "source" option;
2000-08-30 wenzelm 2000-08-30 token trans: removed \mbox to achieve proper italic correction;
2000-08-30 wenzelm 2000-08-30 added string_of;
2000-08-30 nipkow 2000-08-30 introduced induct_thm_tac
2000-08-30 nipkow 2000-08-30 *** empty log message ***
2000-08-30 wenzelm 2000-08-30 tuned;
2000-08-30 wenzelm 2000-08-30 use polyml-version;
2000-08-30 nipkow 2000-08-30 *** empty log message ***
2000-08-30 nipkow 2000-08-30 *** empty log message ***
2000-08-30 wenzelm 2000-08-30 fixed name;
2000-08-30 berghofe 2000-08-30 New function name_of_typ.
2000-08-30 berghofe 2000-08-30 Improved names for size function.
2000-08-30 wenzelm 2000-08-30 fixed comment;
2000-08-30 nipkow 2000-08-30 *** empty log message ***
2000-08-30 nipkow 2000-08-30 Fixed rulify. As a result ?-vars in some recdef induction schemas were renamed.
2000-08-29 wenzelm 2000-08-29 added ML-Systems/polyml-4.0.ML;
2000-08-29 wenzelm 2000-08-29 added \<dots> syntax;
2000-08-29 wenzelm 2000-08-29 added prems_limit;
2000-08-29 wenzelm 2000-08-29 added "name" antiq and "indent" option;
2000-08-29 wenzelm 2000-08-29 pr: added prems limit;
2000-08-29 wenzelm 2000-08-29 added indent;
2000-08-29 wenzelm 2000-08-29 \<dots> syntax;
2000-08-29 wenzelm 2000-08-29 added antiquotation 'name' and option 'indent';
2000-08-29 wenzelm 2000-08-29 'syntax': improved mode spec; 'pr': prems limit;
2000-08-29 wenzelm 2000-08-29 improved spacing of Sum, Prod, integral; tuned;
2000-08-29 wenzelm 2000-08-29 underscore: added \mbox to avoid hyphenation;
2000-08-29 wenzelm 2000-08-29 * 'pr' command: optional argument for ProofContext.prems_limit;
2000-08-29 nipkow 2000-08-29 *** empty log message ***
2000-08-29 nipkow 2000-08-29 *** empty log message ***
2000-08-29 nipkow 2000-08-29 *** empty log message ***
2000-08-29 wenzelm 2000-08-29 made SML/XL happy;
2000-08-29 wenzelm 2000-08-29 updated;
2000-08-29 wenzelm 2000-08-29 improved isabellepar env;
2000-08-29 wenzelm 2000-08-29 updated;