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

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;

added eval_thms;

minimal adaptions for Specification.read/check_specification;

proper Specification.read_specification; Attrib.eval_thms;

removed dead code;

declare_constraints: declare (fix) type variables within constraints, but not terms themselves;

made SML/NJ happy

rudimentary support for Haskell

added support for Haskell, OCaml

Efficient_Nat and Pretty_Int integrated with ML_Int

proper Sign operations instead of Theory aliases; tuned functor application;

tuned functor application;

proper Sign operations instead of Theory aliases;

simplified interpretation setup;

size hook

removed redundant global_parse operations; renamed global_XXX to XXX_global;

Syntax.parse/check/read; no export of read/cert_axm;

Syntax.parse/check/read;

* Pure/Syntax: generic interfaces for parsing and type checking; tuned;

Simplified proof due to improved integration of order_tac and simp.

Transitivity reasoner gets additional argument of premises to improve integration with simplifier.

dropped

ML monad support

no cleverness for instance parameters

added conversions for natural numbers

datatype interpretators for size and datatype_realizer

hide successor

fixed haftmann bug

added @{theory_ref};

added @{type_name};

added polymorphic_types;

eliminated ProofContext.read_termTs;

more ML antiqs;

localized { .. } (but only a few thms)

renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;

renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML; replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);

replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);

removed dead code; tuned;

made smlnj happy;

tuned @{cpat};

added read_term_pattern/schematic/abbrev; prepare_patterns: Variable.polymorphic; removed obsolete cert/pats versions;

ProofContext.read_term_pattern;

constrain: canonical argument order; removed obsolete logicT;

tuned;

TypeInfer.constrain: canonical argument order;

tuned ML setup;

tuned one proof so to not run in a loop with the new atom-representation

changed the representation of atoms to datatypes over nats

ProofContext.mode_abbrev;

removed obsolete set_expand_abbrevs (superceded by mode_abbrev); pretty_term_abbrev: silently ignore ill-typed term; gen_bind: set_mode only locally;

certify': proper do_expand argument (which observes force_expand consts) instead of home-grown normalize;

certify: do_expand as explicit argument, actually certify type of abstractions; tuned signature; tuned;

tuned;

added has_abs (from envir.ML);