cvs-copy - make copy of CVS controlled directory hierarchy;

added 'safe' method; 'auto' method: optional parms;

Method.bang_sectioned_args';

replaced writeln by priority;

added bang_sectioned_args';

'declare' made proper command;

priority_fn := decorate_lines; replaced 'message' by 'priority';

added priority, priority_fn;

added "safe" method;

auto method: opt args; tuned;

converted Lambda scripts;

converted;

fixed rulify_prems;

lemmas [mono] = lists_mono;

updated;

fixed make_pp; basic interrupt handling;

improved exit function for polyml-4.0;

tuned

*** empty log message ***

ported HOL/Lambda/ListBeta;

improved handling of messages: do not decorate writeln output;

improved messages;

more polyml choices; tuned;

added some bind_thm

functional LBV style, dead code, type safety -> Isar

MicroJava changed (all of BV -> Isar)

tuned

*** empty log message ***

tuned;

renamed antiquotation 'name' to 'text'; added antiquotation option 'source';

tuned;

added "source" option;

token trans: removed \mbox to achieve proper italic correction;

added string_of;

introduced induct_thm_tac

*** empty log message ***

tuned;

use polyml-version;

*** empty log message ***

*** empty log message ***

fixed name;

New function name_of_typ.

Improved names for size function.

fixed comment;

*** empty log message ***

Fixed rulify. As a result ?-vars in some recdef induction schemas were renamed.

added ML-Systems/polyml-4.0.ML;

added \<dots> syntax;

added prems_limit;

added "name" antiq and "indent" option;

pr: added prems limit;

added indent;

\<dots> syntax;

added antiquotation 'name' and option 'indent';

'syntax': improved mode spec; 'pr': prems limit;

improved spacing of Sum, Prod, integral; tuned;

underscore: added \mbox to avoid hyphenation;

* 'pr' command: optional argument for ProofContext.prems_limit;

*** empty log message ***

*** empty log message ***

*** empty log message ***

made SML/XL happy;

updated;

improved isabellepar env;

updated;

Lambda/InductTermi made new-style theory; tuned;

proper cong setup;

Simplifier.cong_add_global;

cong setup now part of Simplifier;

updated cong stuff;

'cong' modifiers;

\isakeywordcharunderscore;

* Isar/Provers: 'simp' method now supports 'cong' modifiers; * Provers: Simplifier.easy_setup; tuned;

tex_index: Latex.tex_trailer;

added tex_trailer;

removed METHOD0; added SIMPLE_METHOD('); added thm_args;

Method.SIMPLE_METHOD';

'induct_tac' / 'case_tac': Method.goal_args';

added 'split' method;

\newenvironment{isabellebody}: version without trivlist;

* \isabellestyle{it} produces near math mode output; * settings: smart setup of canonical ML_HOME, ISABELLE_INTERFACE, XSYMBOL_HOME;

Removed map_compose from simpset.

fixed Id string

updated;

restart_loader: reset_path;

add_path: del_path first;

proper setup of iman.sty/extra.sty/ttbox.sty;

updated;

moved \tt things to ttbox.sty; removed \Pure etc;

proper setup;

removed ttbox;

*** empty log message ***

*** empty log message ***

added \trivlist...\endtrivlist to the "isabelle" environment in order to correct several problems (e.g. need for newlines and %)

moved congruence rules UN_cong, INT_cong from UNTIY/Union to Set.ML

xsymbols for {| and |}

xsymbols for leads-to and Join

fixed strip_assums and assum_pairs, restoring them (essentially) to their 1989 versions. They had been "optimized" for flattened parameters, but failed when given an initial, non-flattened proof state. A manifestation of the bug is Goal "of the bug isf. EX B. Q(f,B) ==> (of the bug isy. P(f,y))"; be exE 1;

added some xsymbols, and tidied

more symbols;

disabled trivlist (causes non-descript problems in HOL-Real-HahnBanach);

choosefrom: support easy settings;

choosefrom: easy settings;

isabelle env: trivlist;

removed redundant commands

removed most "makeatother", no longer needed

updated to latest versions of ttbox and ttbreak

updated;

updated;

updated;

tuned translations;

*** empty log message ***

added \isastyleminor; more \isachars; added \isadigit; improved \isakeyword; tuned;

more \isachars; added \isadigit; simplified command markup;

fixed has_meta_prems: strip_assums_hyp;

*** empty log message ***

updated;

open cases;

output \isachar;

cond_add_path;