tuned Defs interfaces;

yet another re-implementation: . maintain explicit mapping from unspecified to specified consts (no dependency graph, no termination check, but direct reduction of specifications); . more precise checking of LHS patterns -- specialized patterns (e.g. 'a => 'a instead of general 'a => 'b) impose global restrictions;

removed obsolete partition (cf. List.partition); tuned;

class axiomatization: finals;

abs: precise typing;

added syntax for 'unchecked';

primrec (unchecked);

List.partition;

ax_derivs: precise typing;

pow: unchecked;

removed obsolete 'finalconsts';

* Pure: syntax 'CONST name' produces a fully internalized constant; tuned;

added CONST syntax; tuned interfaces;

export generic term_syntax;

consts: replaced early'' flag by inverted authentic''; tuned interfaces;

added mapping;

replaced early'' flag by inverted authentic'';

renamed CONST to CONSTANT;

removing the string array from the result of get_clasimp_atp_lemmas

const_syntax;

always preserve authentic consts -- removed Syntax.mixfix_const;

tuned;

removed outdated/redundant comments;

prefer 'definition' over low-level defs; tuned source/document;

tuned source/document;

hide const subst;

tuned;

const_syntax;

* Isar/locale: 'const_syntax';

added const_syntax(_i);

export consts_of; added add_const_syntax; tuned interface;

replaced abbrevs by term_syntax, which is both simpler and more general;

added syntax interface; tuned interface;

added add_modesyntax; tuned;

added 'const_syntax';

added add_const_syntax, add_consts_authentic; tuned interface;

added syntax interface;

tuned concrete syntax -- abbreviation/const_syntax;

updated;

updated;

* Pure/library: divide_and_conquer; * Theory Real: new method ferrack;

replaced references to the robot by the mailing list page

added a much simpler proof for the iteration and recursion combinator - this also fixes a bug which prevented the nightly build from being build (sorry)

Amine Chaieb: Ferrante and Rackoff Algorithm;

Sign.certify_sort;

tuned;

removed low-level str_of_sort/typ/term (use Display.raw_string_of_sort/typ/term instead, or even PolyML.print -- for debugging purposes);

avoid low-level Term.str_of_term;

abstract interfaces for type algebra; tuned;

added divide_and_conquer combinator (by Amine Chaieb); removed remains of old option type; removed obsolete eq_opt; removed obsolete string_of_bool (use Bool.toString instead); tuned;

added low-level string_of_term (back again from term.ML) -- should avoid this altogether;

more abstract interface to classes/arities;

replaced low-level Term.str_of by Display.raw_string_of_term (should actually use Display.string_of_term);

added Ferrante and Rackoff Algorithm -- by Amine Chaieb;

fixed handling of absolute urls

added the lemmas pt_fresh_aux and pt_fresh_aux_ineq (they are used in the proof of the strong induction principle) added code to nominal_atoms to collect these lemmas in "fresh_aux" instantiated for each atom type deleted the fresh_fun_eqvt from nominal_atoms, since fresh_fun is not used anymore in the recursion combinator

reactivated translations for less/less_eq;

added add_primrec_unchecked_i;

unchecked definitions;

defs (unchecked overloaded), including former primrec; tuned;