pretty: do not exterm thm names;

forall_intr_list: do not ignore errors;

separate checks for acyclic/wellformed;

freeze_spec: gensym;

tuned;

axiomatization java_lang;

Changed the DFG format's functions' declaration procedure.

Fixed a bug.

A new "spass" method.

Added in settings used by "spass" method.

Added in SPASS oracle.

HOL problems now have DFG output format.

Changed input interface of dfg_write_file.

Added support for DFG format, used by SPASS.

Helper files in DFG format.

add_datatype_axm: finalize specified consts;

tuned;

tuned;

made smlnj happy;

wellformed: be less ambitious about structural containment; tuned;

Pure: update on overloaded defs;

Extended strong induction rule with additional freshness constraints.

add theorem cfcomp_strict

added add_deps, which actually records dependencies of consts (unlike add_finals); tuned;

tuned;

axiomatize class: Theory.add_deps;

simplified info/get_info; Rep/Abs: Theory.add_deps; tuned;

simplified TypedefPackage.get_info;

made smlnj happy;

pretty_full_theory: tuned output of definitions;

export plain_args; tuned wellformed, normalize;

Defs.specifications_of: lhs/rhs now use typargs;

removed unchecked'';

pretty_full_theory: defs;

specifications_of: lhs/rhs represented as typargs; export pretty_const; export dest; more precise checking of lhs patterns; more precise normalization; misc cleanup;

export raw_unifys, could_unifys;

made smlnj happy;

export raw_matches;

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;

updated;

add_defs: unchecked flag; tuned;

'defs': unchecked flag;

Theory.add_defs(_i): added unchecked flag;

added add_defs_unchecked(_i);

actually reject malformed defs; added unchecked flag; tuned;

moved defs explanation to isar-ref;

added defs (unchecked)''; more explanations on well-formednes of defs;

* Pure: overloaded definitions are now actually checked for acyclic dependencies;

tuned;

added lemma in_measure

fixed silly bug in function serializer for ML

add new finite chain theorems

improved propagate_deps; removed structs_less, which is actually unsound in conjunction with interdependent overloaded consts;

check result against certified prop, i.e. admit non-normal statements;

tuned;

avoid raw equality on type thm;

replaced Graph.fold_nodes by general Graph.fold;

added fold; removed fold_nodes; added IntGraph; tuned;

tuned Defs.merge;

allow dependencies of disjoint collections of instances; major cleanup;

use IntGraph from Pure;