2006-05-25 wenzelm 2006-05-25 axiomatization java_lang;
2006-05-25 mengj 2006-05-25 Changed the DFG format's functions' declaration procedure.
2006-05-25 mengj 2006-05-25 Fixed a bug.
2006-05-25 mengj 2006-05-25 A new "spass" method.
2006-05-25 mengj 2006-05-25 Added in settings used by "spass" method.
2006-05-25 mengj 2006-05-25 Added in SPASS oracle.
2006-05-25 mengj 2006-05-25 HOL problems now have DFG output format.
2006-05-25 mengj 2006-05-25 Changed input interface of dfg_write_file.
2006-05-25 mengj 2006-05-25 Added support for DFG format, used by SPASS.
2006-05-25 mengj 2006-05-25 Helper files in DFG format.
2006-05-24 wenzelm 2006-05-24 add_datatype_axm: finalize specified consts;
2006-05-24 wenzelm 2006-05-24 tuned;
2006-05-24 wenzelm 2006-05-24 tuned;
2006-05-24 wenzelm 2006-05-24 made smlnj happy;
2006-05-24 wenzelm 2006-05-24 wellformed: be less ambitious about structural containment; tuned;
2006-05-24 wenzelm 2006-05-24 Pure: update on overloaded defs;
2006-05-24 berghofe 2006-05-24 Extended strong induction rule with additional freshness constraints.
2006-05-24 huffman 2006-05-24 add theorem cfcomp_strict
2006-05-24 wenzelm 2006-05-24 added add_deps, which actually records dependencies of consts (unlike add_finals); tuned;
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;