added nth_drop

tuned datatype_codegen setup

certificates for code generator case expressions

added illustrative diagnostics

clarified declarations in class ord

concept for exceptions

clarified name suffix

step towards proper purge operation

put declarations first

clarified terminology

intermediate cleanup

clarified relationship of code generator conversions and evaluations

abs_conv/forall_conv: proper context (avoid gensym); removed unused cache_conv;

load variable.ML before conv.ML;

Conv.forall_conv: proper context;

cover AFP logs as well, using "afp" pseudo-platform;

moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;

avoid gensym;

updated Sign.add_abbrev;

combinator translation

avoid unnamed infixes;

avoid unnamed infixes; tuned;

avoid unnamed infixes;

modernized specifications; tuned proofs;

mark inductive results as internal;

skolem_cache: ignore internal theorems -- major speedup; skolem_cache_theorems_of: efficient folding of table; replaced get_axiom by Thm.get_axiom_i (avoids name space fishing);

major speedup by avoiding metis;

modernized definitions;

added add_defs_new, which strips sorts for axioms (presently inactive);

removed unused add_defss;

tuned internal inductive interface;

tuned internal interfaces: flags record, added kind for results; tuned;

inductive: mark internal theorems as Thm.internalK;

tuned;

export tsig_of;

clarified role of class relations

ignore mutual recursive modules

integer compatibility: added wrapper for structure Time;

fixed use_text;

downgraded IntInf with divMod; fixed use_text;

added auto-quickcheck-time-limit;

auto_quickcheck: pervasive options, turned time_limit into plain int, simplified exception handling;

added auto_quickcheck feature;

Norbert Schirmer: record improvements;

preliminary material for Isabelle2007;

misc tuning and update;

misc tuning and update;

misc tuning and update;

updated year to 2007;

tuned;

added some lemmas

print_state_context: local theory context, not proof context; context_position: cover Theory case as well (requires additional checkpoint);

ContextPosition.put_ctxt;

NameSelection: more interval checks;

tuned message;

turned into generic context data;

ML_setup for bind_thms;

Simplified interface for printing of interpretations.

unfold_locales workaround

Theory/context data restructured; simplified interface for printing of interpretations.

fixed dir in single-logic test

llabs/sko: removed Name.internal;

avoid unnamed infixes;

avoid internal names;

switch notification email back on

fix shell quoting confusion

local_theory transactions: more careful treatment of context position;

keep context position as tags for consts/thms;

add_abbrev: tags (Markup.property list);

added internalK, property_internal;

add_consts_authentic/add_abbrev: tags (Markup.property list); tuned signature;

Markup.internalK;

print_theory: observe Markup.internal_property of consts, discontinued special treatment of internal names elsewhere;

added properties_of;

maintain tags (Markup.property list); tuned;

skofuns/absfuns: explicit markup as internal consts;

Sign.add_consts_authentic: tags (Markup.property list);

standard_term_check: include expand_abbrevs (back again);

added unparse interfaces (still unused); add_typ/term_check: added stage and name argument; added print_checks;

removed redundant const_constraint; add_const_constraint: proper certification; prepare_dummies: avoid imperative features; term_check: separate phases, standard_infer_types passes inference parameters instead of frees/vars; Syntax.install_operations: dummy unparsers;

Sign.add_const_constraint; Syntax.add_typ/term_check: added stage and name argument;

maintain maxidx (analogous to name context); polymorhic: observe Variable.maxidx_of;

added fixate_params; type_infer: freeze_mode = NONE keeps inference parameters in result; type_infer: observe Variable.maxidx_of;

Sign.the_const_constraint;

added declare_typ_names; replace_dummy_patterns: canonical argument order;

removed obsolete external interface add_const_constraint; removed redundant const_constraint; renamed add_const_constraint_i to add_const_constraint;

Sign.add_const_constraint;

fixed metis proof (Why did it stop working?);

swapped machines for at-sml-dev and at-sml-dev-p

no proof terms for smlnj

add -p 2 at-sml-dev test for HOL proof terms sessions only

at-sml-dev session with -p 2

Added target for proof term sessions (those that need -p 2)

accept single logic and target as argument

exported constraint interfaces

exported intern_expr

added ocaml strings

further localization

proper syntax during class specification

prove_strong_ind now uses InductivePackage.rulify.

Adapted to changes in interface of add_inductive_i.

add_inductive_i now takes typ instead of typ option as argument.

- add_inductive_i now takes typ instead of typ option as argument - close_rule is now applied before expanding abbreviations - rulify applies norm_hhf again

proper handling of chained facts;

removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering theorems of Nat.thy are hidden by the Ordering.thy versions

Fixed setup of transitivity reasoner (function decomp).

some more simultaneous use_thys;

read: explicit treatment of scanner failure;

tuned;

tuned;

tuned;

* Pure/Isar: unified specification syntax admits type inference and dummy patterns; print mode: no_abbrevs;

read/check_specification: free_dummy_patterns;

added free_dummy_patterns;

added minimize_sort, complete_sort;

Sign.minimize/complete_sort;

convenient obtain rule for sets

added code lemma for 1

moved Finite_Set before Datatype

adapted variable order for inductive cases (determined by read_specification *before* expanding abbreviations);