goals_limit moved to display.ML;

added goals_limit (from tctical.ML); added pretty_goals_aux, removed excessive variants of print_goals;

use_thy "Locales";

use locales instead of consts/axioms;

* Isar/Pure: proper integration with ``locales''; unlike the original version by Florian Kammueller, Isar locales package high-level proof contexts rather than raw logical ones (e.g. we admit to include attributes everywhere); * Isar/Pure: theory goals now support ad-hoc contexts, which are discharged in the result, as in ``lemma (assumes A and B) K: A .''; syntax coincides with that of a locale body;

activate dead code, make document work;

renamed Sqrt_Irrational.thy to Sqrt.thy;

Locales and simple mathematical structures;

renamed Real/ex/Sqrt_Irrational.thy to Real/ex/Sqrt.thy; added ex/Locales.thy;

extend_XXX: sane argument order ... -> syntax -> syntax;

local syntax: add_syntax, proper read/pretty functions;

locale_element/uses: string;

proper treatment of local syntax; store_thm: test atts; Uses: string;

print_syntax: include local version;

added pretty_term', read_typ', read_typ_no_norm', read_def_terms' which refer to local syntax;

export pretty_thm_aux;

tuned;

theorem(_i): locale atts; global_goal, finish_global: proper treatment of target locale;

group locale_element;

added add_locale(_i) and store_thm; removed old scope stuff; tuned;

theorem(_i): locale atts; added add_locale;

added 'locale', 'print_locales', 'print_locale';

added print_locales, print_locale;

added "locale", "print_locale", "print_locales";

fixes: optional typ; removed garbage;

added pretty/print functions with context; added cert_def; print_asms covers both fixes and assumes;

locale_element: optional typ;

pretty/print functions with context;

export add_tvarsT, add_tvars, add_vars, add_frees (would actually belong to term.ML, but is apt to cause some confusion with the fold-right versions there);

Method.trace ctxt;