adapted PThm;

proof_of_term: removed obsolete disambiguisation table; adapted PThm; Thm.proof_of returns proof_body;

rewrite_proof: simplified simprocs (no name required); adapted PThm; fold_proof_atoms;

Thm.proof_of returns proof_body; adapted PThm;

refined notion of derivation, consiting of promises and proof_body; removed oracle_of (would require detailed check wrt. promises); proof_of returns proof_body;

reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial); added type proof_body, which covers oracles and thms of local proof; added general fold_body_thms, fold_proof_atoms; removed thms_of_proof, thms_of_proof', axms_of_proof; slightly more abstract handling of body content (oracles, thms); rewrite_proof: simplified simprocs (no name required); thm_proof: lazy fulfillment of promises;

pretty_thm: oracle flag is always false for now (would require detailed check wrt. promises);

ProofSyntax.proof_of_term: removed obsolete disambiguisation table; adapted PThm;

name_of_thm: Proofterm.fold_proof_atoms; Thm.proof_of returns proof_body;

Thm.proof_of returns proof_body;

clean: added HOL-Main;

rewrite_proof: simplified simprocs (no name required);

multithreading support for polyml-5.2 actually disabled -- as advertized;

Initial part of locale reimplementation.

Made local_note_prefix public.

re-educated guess

namify and name_decl combinators

Name.is_nothing

lemmas about dom and minus / insert

added length_unique operation for code generation

updated generated files;

removed "includes" element (lost update?);

updated generated files;

added section "Explicit instantiation within a subgoal context";

renamed "Rules" to "Object-level rules";

more on basic tactics;

basic ML reference for tactics;

added section "Tactics";

more contributors;

separate section "Inspecting the syntax" for print_syntax;

misc tuning of inner syntax;

added inner lexical syntax, reusing outer one;

misc tuning;

tuned outer lexical syntax; fixed var/tvar: really need question marks here;

more tuning of Pure grammer;

updated and elaborated Pure grammer;

added Pure grammer (from old ref manual);

mixfix annotations: verbatim for special symbols;

added section "The Pure grammar" (incomplete version, based on old ref manual);

added section "Priority grammars" (variant from old ref manual);

added section "Co-regularity of type classes and arities" (variant from old ref manual); tuned arity spacing;

minor tuning (according to old ref manual);

misc tuning and rearrangement of section "Printing logical entities";

misc tuning and rearrangement of section "Printing logical entities";

fixed/tuned syntax for attribute "tagged";

added pretty printing options (from old ref manual);

separate chapter "Inner syntax --- the term language";

updated/refined types of Isar language elements, removed special LaTeX macros;

unified use of declaration environment with IsarImplementation; tuned ML decls;

ignore ThyOutput.source flag;

added bind_thm, bind_thms;

tuned section "Incorporating ML code"; moved method_setup to separate section "Defining proof methods";

tuned section "Oracles";

tuned section arrangement;

moved section "Proof method expressions" to proof chapter; minor rearrangement of proof sections;

more on mixfix annotations (updated material from old ref manual);

tuned;

moved section "Document preparation" to front;

updated section "Markup via command tags";

renamed "formal comments" to "document comments"; tuned section "Markup commands"; updated/tuned section "Document Antiquotations";

renamed "formal comments" to "document comments";

tuned "Markup commands";

tuned intro of "Document preparation";

reworked "Defining Theories";

removed Assert.thy

dropped superfluos eval_conv

moved assert to Heap_Monad.thy

simproc for let

improved handling of !!/==> for eval and normalization

proper name morphisms for locales

consider prefixes for name bindings of simprocs (a first approximation)

diagnostic output for name bindings

Some modifications in code for proving arities to make it work for datatype definitions with additional sort constraints.

min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf

restruced naming code in anticipation of introduction of name morphisms

more verbose element printing

clarified comment

Added support for parametric datatypes.

Streamlined functions for accessing information about atoms.

Some more functions for accessing information about atoms.

Made doc compatible with the system.

clarified verbatim vs. typewriter

using explicit interpretaton prefix in Name.binding (still on the surface)

explicit interpretation prefix in Name.binding

tuned

exported codegen_preproc

Minor cleanup.

Keyword 'includes' gone.

tuned

added lemma

Added second tiling example.

cleaned

tuned

class morphism stemming from locale interpretation

improved verbatim mechanism

Theorem "_" is now stored with open derivation.