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.

Removed argument prf2 in rewrite rules for equal_elim to make them applicable to eta-contracted proofs.

Replaced arbitrary by undefined.

Dropped context element 'includes'.

adapted to strict pattern discipline

explicit check for pattern discipline before code translation

Revoked workaround (incompatible with HOL/ex/LocaleTest2.thy).

restored incremental code generation

slightly tuned

assert that no class parameter is used as constructor

cleanup code default attribute

removed includes

making SMLNJ happy

The metis method no longer fails because the theorem is too trivial

Removed 'includes meta_term_syntax' and 'includes meta_conjunction_syntax'.

metis proof

New-style locale expressions with instantiation (new file expression.ML).

Hide path in constant name (workaround).

explicit history for equations; tuned

slightly tuned

added rudimentary code generation

sup_bot and inf_top

Extension of interface: declarations_of.

simplified user-defined class syntax

more clever module names for code generation

"fun" gained a more uniform status

simplified syntax for class parameters

tuned

new classes "top" and "bot"

tuned proof

more clever module name aliasses for code generation

"arbitrary" merely abbreviates undefined

subst is a proper axiom again

updated

explicit namings for generated code

Thm.get_def;

Thm.def_name;

multithreading support only for polyml-5.2.1 or later;

renamed get_axiom_i to axiom, removed obsolete get_axiom; reduced pervasive names;

renamed Thm.get_axiom_i to Thm.axiom;

renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;