2006-05-20 wenzelm 2006-05-20 ax_derivs: precise typing;
2006-05-20 wenzelm 2006-05-20 pow: unchecked;
2006-05-20 wenzelm 2006-05-20 removed obsolete 'finalconsts';
2006-05-17 wenzelm 2006-05-17 * Pure: syntax 'CONST name' produces a fully internalized constant; tuned;
2006-05-17 wenzelm 2006-05-17 added CONST syntax; tuned interfaces;
2006-05-17 wenzelm 2006-05-17 export generic term_syntax;
2006-05-17 wenzelm 2006-05-17 consts: replaced early'' flag by inverted authentic''; tuned interfaces;
2006-05-17 wenzelm 2006-05-17 added mapping;
2006-05-17 wenzelm 2006-05-17 replaced early'' flag by inverted authentic'';
2006-05-17 wenzelm 2006-05-17 renamed CONST to CONSTANT;
2006-05-17 paulson 2006-05-17 removing the string array from the result of get_clasimp_atp_lemmas
2006-05-17 wenzelm 2006-05-17 const_syntax;
2006-05-17 wenzelm 2006-05-17 always preserve authentic consts -- removed Syntax.mixfix_const;
2006-05-17 wenzelm 2006-05-17 tuned;
2006-05-17 wenzelm 2006-05-17 removed outdated/redundant comments;
2006-05-17 wenzelm 2006-05-17 prefer 'definition' over low-level defs; tuned source/document;
2006-05-17 wenzelm 2006-05-17 tuned source/document;
2006-05-16 wenzelm 2006-05-16 hide const subst;
2006-05-16 wenzelm 2006-05-16 tuned;
2006-05-16 wenzelm 2006-05-16 const_syntax;
2006-05-16 wenzelm 2006-05-16 * Isar/locale: 'const_syntax';
2006-05-16 wenzelm 2006-05-16 added const_syntax(_i);
2006-05-16 wenzelm 2006-05-16 export consts_of; added add_const_syntax; tuned interface;
2006-05-16 wenzelm 2006-05-16 replaced abbrevs by term_syntax, which is both simpler and more general;
2006-05-16 wenzelm 2006-05-16 added syntax interface; tuned interface;
2006-05-16 wenzelm 2006-05-16 added add_modesyntax; tuned;
2006-05-16 wenzelm 2006-05-16 added 'const_syntax';
2006-05-16 wenzelm 2006-05-16 added add_const_syntax, add_consts_authentic; tuned interface;
2006-05-16 wenzelm 2006-05-16 added syntax interface;
2006-05-16 wenzelm 2006-05-16 tuned concrete syntax -- abbreviation/const_syntax;
2006-05-16 wenzelm 2006-05-16 updated;
2006-05-16 wenzelm 2006-05-16 updated;
2006-05-16 wenzelm 2006-05-16 * Pure/library: divide_and_conquer; * Theory Real: new method ferrack;
2006-05-16 paulson 2006-05-16 replaced references to the robot by the mailing list page
2006-05-16 urbanc 2006-05-16 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)
2006-05-16 wenzelm 2006-05-16 Amine Chaieb: Ferrante and Rackoff Algorithm;
2006-05-16 wenzelm 2006-05-16 Sign.certify_sort;
2006-05-16 wenzelm 2006-05-16 tuned;
2006-05-16 wenzelm 2006-05-16 removed low-level str_of_sort/typ/term (use Display.raw_string_of_sort/typ/term instead, or even PolyML.print -- for debugging purposes);
2006-05-16 wenzelm 2006-05-16 avoid low-level Term.str_of_term;
2006-05-16 wenzelm 2006-05-16 abstract interfaces for type algebra; tuned;
2006-05-16 wenzelm 2006-05-16 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;
2006-05-16 wenzelm 2006-05-16 added low-level string_of_term (back again from term.ML) -- should avoid this altogether;
2006-05-16 wenzelm 2006-05-16 more abstract interface to classes/arities;
2006-05-16 wenzelm 2006-05-16 replaced low-level Term.str_of by Display.raw_string_of_term (should actually use Display.string_of_term);
2006-05-16 wenzelm 2006-05-16 added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
2006-05-16 haftmann 2006-05-16 fixed handling of absolute urls
2006-05-15 urbanc 2006-05-15 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
2006-05-13 wenzelm 2006-05-13 reactivated translations for less/less_eq;
2006-05-13 wenzelm 2006-05-13 added add_primrec_unchecked_i;
2006-05-13 wenzelm 2006-05-13 unchecked definitions;
2006-05-13 wenzelm 2006-05-13 defs (unchecked overloaded), including former primrec; tuned;
2006-05-13 wenzelm 2006-05-13 updated;
2006-05-13 wenzelm 2006-05-13 add_defs: unchecked flag; tuned;
2006-05-13 wenzelm 2006-05-13 'defs': unchecked flag;
2006-05-13 wenzelm 2006-05-13 Theory.add_defs(_i): added unchecked flag;
2006-05-13 wenzelm 2006-05-13 added add_defs_unchecked(_i);
2006-05-13 wenzelm 2006-05-13 actually reject malformed defs; added unchecked flag; tuned;
2006-05-13 wenzelm 2006-05-13 moved defs explanation to isar-ref;
2006-05-13 wenzelm 2006-05-13 added defs (unchecked)''; more explanations on well-formednes of defs;