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);

Attrib.eval_thms; Syntax.parse/check;

Attrib.eval_thms;

read/check_specification: proper type inference across multiple sections, result is in closed form; added read/check_free_specification for single section, non-closed form;