* The ML antiquotation prints type-checked ML expressions verbatim.

replace freeze by 'setmp show_question_marks false';

proof_to_theory_context: interaction flag;

accomodate interface Proof vs. Method;

added NO_CASES;

moved after method.ML; moved FINDGOAL/HEADGOAL to method.ML; moved type method to method.ML; prepare attributes here; tuned various interfaces (cf. isar_thy.ML); tuned;

prepare attributes here; tuned;

moved before proof.ML; added FINDGOAL/HEADGOAL (from proof.ML); added type method (from proof.ML); moved proof refinement etc. to proof.ML; tuned;

added add_locale_context(_i), which returns the body context for presentation; note_thmss(_i), add_thmss: returns context for presentation; removed map_attrib_specs/facts (cf. Attrib.map_specs/facts);

moved translation functions to Pure/sign.ML; moved attribute preparation to actual operations in proof.ML etc.; removed various trivial interfaces;

various Toplevel.theory_context commands: proper presentation in context; simplified interfaces Proof vs. IsarThy;

use theory instead of obsolete Sign.sg; tuned comments;

added map_specs/facts operators (from locale.ML);

removed obsolete Theory.sign_of;

load method.ML before proof.ML;

added interfaces for compile translation functions (from Isar/isar_thy.ML);

added tap;

updated;

usedir: tuned option -V;

usedir: removed option -H;

* Proper output of proof terms within a proof context; * Proper output of antiquotations for theory commands involving a proof context; * 'print_theorems': in theory mode print difference of facts, in proof mode print local facts;

Improved generation of witnesses in interpretation.

Interpretation in locales.

Use interpretation in locales.