\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;