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

Term.has_abs;

proper signature constraint; minor tuning;

added interrupt_timeout; tuned signature;

Generic interpretation of theory data.

tuned signature; moved generic interpretation to interpretation.ML; added abstract at_begin/end wrappers;

avoid Theory.rep_theory;

added interpretation.ML;

improved error behaviour of use (bootstrap version);

more precise treatment of free dictionary parameters for evaluation

fixed cg setup

restored ml system independence

more permissive

clarified code lemmas

fixed wrong syntax treatment in class target

code lemmas for cardinality

- eval_term no longer computes result during compile time - generated ML code is now compiled via ML_Context.use_mltext rather than use_text; this makes sure that antiquotations are expanded - quickcheck now checks whether types to be substituted for type variables have correct sorts; this avoids spurious counterexamples - execution time for auto_quickcheck is now limited

improved computing

changed lemmas

ml_output: proper error instead of error_msg;

comment added to explain a potential scheduling problem

tuned

*** empty log message ***

metis too slow

move at-sml-dev to 2-processor atbroy100

make sun-sml-dev non-proof-term, and at-sml-def -p 2 (at-sml-dev being moved to faster atbroy100)

Generalized [_.._] from nat to linear orders

Enclosed end_theory in text antiquotation to make LaTeX happy.

* ML: just one true type int;

New diagnostic command print_orders.

Transitivity reasoner set up for locales order and linorder.

Simplified proofs due to transitivity reasoner setup.

Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.

Morphisms applied in global interpretations behave correctly on types and terms.

New function inst_morphism'.

Transitivity reasoner set up for locales.

removed dead/unmaintained code;

simplified PrintMode interfaces;

moved Tools/integer.ML to Pure/General/integer.ML;

metis now available in PreList

reactivated tests in smlnj;

simplified type int (eliminated IntInf.int, integer);

(reverted to previous version)

updated

*** empty log message ***

introduced generic concepts for theory interpretators

separated code for inductive sequences from inductive_codegen.ML

distinction between regular and default code theorems

renamed constructor RealC to Ratreal

renamed constructor RatC to Rational

clarified evaluation code