clarified signature;

more robust declaration of resulting statement text, instead of somewhat accidental (Variable.maybe_bind_term result_binds in generic_goal);

eliminated ASCII syntax from Pure bootstrap;
tuned comments;

tuned signature;

'obtain' supports structured statements (similar to 'define');

more uniform operations for structured statements;

defs are closed, which leads to proper auto_bind_facts;
misc tuning;

clarified modules;

prefer internal attribute source;

more general types Proof.method / context_tactic;
proper context for Method.insert_tac;
tuned;

support for structure statements in 'assume', 'presume';

moved remaining display.ML to more_thm.ML;

added Thm.chyps_of;
eliminated Thm.cprep_thm, with its potentially ill-typed (!) tpairs (cf. c9ad3e64ddcf);

Variable.focus etc.: optional bindings provided by user;
Subgoal.focus command: more careful treatment of user-provided bindings;

simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);

support 'when' statement, which corresponds to 'presume';

more robust: variables need not occur in body;

improved treatment of Element.Obtains via Expression.prepare_stmt;
discontinued pointless all_types ctxt: prep_var is always sequential;

tuned comment;

tuned signature;

open parameters for 'consider' rule;

eliminated slightly odd Element.close_form: toplevel specifications have different policies than proof text elements;

clarified 'obtain', using structured 'have' statement;

tuned comments;

clarified 'consider', using structured 'have' statement;

support for 'consider' command;
allow full "fixes" for 'obtain' command;
tuned signature;

support to parse obtain clause without type-checking yet;
tuned signature;

tuned signature;

clarified local after_qed: result is not exported yet;
proper goal_export for show: 'if' is like 'assume';

support for "if prems" in local goal statements;

more uniform treatment of auto bindings vs. explicit user bindings;
misc tuning;

tuned signature;

allow for_fixes for 'have', 'show' etc.;
tuned signature;

clarified abstracted term bindings (again, see c8384ff11711);

clarified term bindings;

clarified context;

tuned;

clarified abstracted term bindings;

avoid duplicate warning due to Variable.warn_extra_tfrees;

clarified Proof_Context.cert_propp/read_propp;
tuned;

more careful treatment of term bindings in 'obtain' proof body;
tuned signature;

tuned signature;

tuned signature;

tuned signature;

tuned signature;

more explicit context;

proper context for Object_Logic operations;

clarified context;

Thm.cterm_of and Thm.ctyp_of operate on local context;

tuned -- more explicit use of context;

added Proof_Context.cterm_of/ctyp_of convenience;

more position markup to help locating the query context, e.g. from "Info" dockable;

print results as "state", to avoid intrusion into the source text;
print new local theory (again);

proper context for norm_hhf and derived operations;
clarified tool context in some boundary cases;

tuned signature;

Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;

more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;

clarified signature;

display proof results as "state", to suppress odd squiggles in the Prover IDE (see also 9240be8c8c69);

discontinued old-style Term.list_abs in favour of plain Term.abs;

discontinued old-style Term.list_all_free in favour of plain Logic.all;

tuned signature -- avoid spurious Thm.mixed_attribute;

more general Proof_Context.bind_propp, which allows outer parameters;
obtain: some support for term bindings within the proof, depending on parameters;

tuned signature;

tuned signature -- canonical argument order;

discontinued Name.variant to emphasize that this is old-style / indirect;

eliminated slightly odd Proof_Context.bind_fixes;
tuned;

more precise positions via binding;

clarified Variable.focus vs. Variable.focus_cterm -- eliminated clone;

tuned signature -- eliminated odd comment;

more formal treatment of parameters, avoiding slightly odd Variable.intern_fixed;

reorganized fixes as specialized (global) name space;

modernized structure Proof_Context;

tuned signature, disentangled dependencies;

explicit structure Syntax_Trans;
discontinued old-style constrainAbsC;

--HG--
rename : src/Pure/Syntax/syn_trans.ML => src/Pure/Syntax/syntax_trans.ML

renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;

--HG--
rename : src/Pure/meta_simplifier.ML => src/Pure/raw_simplifier.ML

turned show_sorts/show_types into proper configuration options;

tuned messages: discontinued spurious full-stops (messages are occasionally composed unexpectedly);

modernized naming conventions of main Isar proof elements;

renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;

modernized structure Object_Logic;

normalized uncurry take/drop

--HG--
extra : rebase_source : 647c8b5a6641f0eef6d4d81646474d16388f9fb9

curried take/drop

--HG--
extra : rebase_source : 6e6b508d936640bef00f0ad0c4fb089ad5253ef0

modernized structure Proof_Display;

modernized structure AutoBind;

modernized structure Context_Rules;

modernized structure Rule_Cases;

indicate CRITICAL nature of various setmp combinators;

eliminated dead code;

Variable.focus: named parameters;

proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;

renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef -- Alice is no longer supported);
renamed Variable.importT_thms to Variable.importT (again);

renamed ProofContext.add_fixes_i to ProofContext.add_fixes, eliminated obsolete external version;

replaced add_binds(_i) by bind_terms -- internal version only;

use Name.of_binding for basic logical entities without name space (fixes, case names etc.);

Merge.

renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
minor tuning;

Thm.binding;

binding is alias for Binding.T

qed/after_qed: singleton result;

Name.name_of -> Binding.base_name

cleaned up binding module and related code

type Attrib.binding abbreviates Name.binding without attributes;
Attrib.no_binding refers to Name.no_binding;

explicit type Name.binding for higher-specification elements;
simplified ProofContext.inferred_param;

generic Syntax.pretty/string_of operations;

renamed Variable.import to import_thms (avoid clash with Alice keywords);

export: added explicit term operation;

qualified MetaSimplifier.norm_hhf(_protect);

moved statement to specification.ML;

statement: Variable.fix_frees;

added tactical result;
simplified obtain_export: no Seq.seq, no lifting of result prems;
tuned;

moved basic assumption operations from structure ProofContext to Assumption;

Variable.import(T): result includes fixed types/terms;

added find_free (from term.ML);

replaced Term.variant(list) by Name.variant(_list);
Name.internal;

guess: proper context for polymorphic parameters;
tuned;

obtain_export: Thm.generalize;
guess: fixed handling of mixfixes of vars;
tuned;

Term.internal;

ProofContext: moved variable operations to struct Variable;

fixes: include mixfix syntax;

guess: more careful about local polymorphism;
guess: explicit term vars in statement (avoids warning);

removed 'concl is' patterns;

tuned basic list operators (flat, maps, map_filter);

subtract (op =);

Proof.refine_insert;
statements: always use Attrib.src;

obtain(_i): optional name for 'that';
added statement (cf. Locale.theorem);

tuned comments;

ProofContext.inferred_param;

simplified type attribute;

guess: used fixed inferred_type of vars;

sane ERROR handling;

uniform handling of fixes;

generic attributes;

Term.betapplys;

guess: Seq.hd;
Term.find_free;

simplified after_qed;

renamed Goal constant to prop, more general protect/unprotect interfaces;

improved check_result;
Goal.init, Goal.conclude;

tuned error msg;
tuned;

added 'guess', which derives the obtained context from the course of reasoning;

tuned Isar proof elements;

prepare attributes here;
tuned;

After_qed takes result argument.

tuned;

(intermediate commit)

no Syntax.internal on thesis;

Move towards standard functions.

Deleted Library.option type.

Merged in license change from Isabelle2004

improved messages;

Syntax.internal thesis;

renamed rule_context.ML to context_rules.ML;

RuleContext.intro_query_local;

Proof.have_i: multiple statements;

pretty/print functions with context;

improved source arrangement of obtain;

simplified exporter interface;

use ObjectLogic;

comment

fixed binding of parameters;

tuned statement args;

improved handling of "that": insert into goal, only declare as Pure "intro";
eliminated functor;

tuned;

turned into plain context element;
exporter setup;

bind_skolem;

GPLed;

ProofContext.find_free;

handle general case: params and hyps of thesis;

obtain: renamed 'in' to 'where';

ObtainFun;
prepare vars / asms / pats only once;

warn_extra_tfrees;

tuned comment;

The 'obtain' language element -- achieves (eliminated) existential
quantification proof command level.