2006-05-24 wenzelm 2006-05-24 tuned;
2006-05-24 wenzelm 2006-05-24 axiomatize class: Theory.add_deps;
2006-05-24 wenzelm 2006-05-24 simplified info/get_info; Rep/Abs: Theory.add_deps; tuned;
2006-05-24 wenzelm 2006-05-24 simplified TypedefPackage.get_info;
2006-05-23 wenzelm 2006-05-23 made smlnj happy;
2006-05-23 wenzelm 2006-05-23 pretty_full_theory: tuned output of definitions;
2006-05-23 wenzelm 2006-05-23 export plain_args; tuned wellformed, normalize;
2006-05-22 wenzelm 2006-05-22 Defs.specifications_of: lhs/rhs now use typargs;
2006-05-22 wenzelm 2006-05-22 removed unchecked'';
2006-05-22 wenzelm 2006-05-22 pretty_full_theory: defs;
2006-05-22 wenzelm 2006-05-22 specifications_of: lhs/rhs represented as typargs; export pretty_const; export dest; more precise checking of lhs patterns; more precise normalization; misc cleanup;
2006-05-22 wenzelm 2006-05-22 export raw_unifys, could_unifys;
2006-05-20 wenzelm 2006-05-20 made smlnj happy;
2006-05-20 wenzelm 2006-05-20 export raw_matches;
2006-05-20 wenzelm 2006-05-20 tuned Defs interfaces;
2006-05-20 wenzelm 2006-05-20 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;
2006-05-20 wenzelm 2006-05-20 removed obsolete partition (cf. List.partition); tuned;
2006-05-20 wenzelm 2006-05-20 class axiomatization: finals;
2006-05-20 wenzelm 2006-05-20 abs: precise typing;
2006-05-20 wenzelm 2006-05-20 added syntax for 'unchecked';
2006-05-20 wenzelm 2006-05-20 primrec (unchecked);
2006-05-20 wenzelm 2006-05-20 List.partition;
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;