Commands prf and full_prf can now also be used to display proof term of current proof state.

eliminated old "symbols" syntax, use "xsymbols" instead;

theory data: finish method;

indexvar_ast_tr (for \<index> placeholder);

removed pure_sym_syntax; allow additional arguments in infixes (maximum priority);

File.use;

added impose_hyps_tac; robustify insts of tactic emulations;

proper close_locale;

no longer support "isabelle_font" or "symbols";

got rid of obsolete input filtering;

back to normal; tuned;

eliminated old "symbols" syntax, use "xsymbols" instead;

updated;

got rid of obsolete input filtering and isabelle font encoding;

got rid of obsolete input filtering;

eliminated old "symbols" syntax, use "xsymbols" instead;

theory data: finish method;

removed needs_filtered_use;

\newcommand{\isasymindex}{\isamath{\i}};

* Isar/Pure: emulation of instantiation tactics (rule_tac, cut_tac, etc.) now consider the syntactic context of assumptions, giving a better chance to get type-inference of the arguments right (this is especially important for locales); * system: refrain from any attempt at filtering input streams; no longer support ``8bit'' encoding of old isabelle font, instead proper iso-latin characters may now be used;

tuned;

\bibliographystyle{abbrv};

updated;

make SML/XL of NJ happy;

ex/document/root.bib;

proper syntax for structs;

more explanations on advanced syntax;

use num_const of Pure;

\newcommand{\isasymstruct}{\isamath{\diamond}};

locale_prefix: Sign.base_name;