2006-07-25 wenzelm 2006-07-25 added find_free (from term.ML);
2006-07-25 wenzelm 2006-07-25 added is/to_ascii_lower/upper; tuned alphanum -- needs more work;
2006-07-25 wenzelm 2006-07-25 is_funtype: do not export internal operation; added add_varnames (cf. add_vars etc.); removed obsolete (add_)term_varnames; removed find_free (moved to Isar/obtain.ML); moved variant_abs to structure Syntax -- this is a syntax operation after all;
2006-07-25 wenzelm 2006-07-25 tuned;
2006-07-25 wenzelm 2006-07-25 use Term.add_vars instead of obsolete term_varnames;
2006-07-25 wenzelm 2006-07-25 renamed add_term_varnames to Term.add_varnames (cf. Term.add_vars etc.);
2006-07-25 wenzelm 2006-07-25 tuned ML code;
2006-07-25 wenzelm 2006-07-25 renamed Term.variant_abs to Syntax.variant_abs;
2006-07-25 wenzelm 2006-07-25 Drule.merge_rules;
2006-07-25 haftmann 2006-07-25 renamed Name.give_names to Name.names and moved Name.alphanum to Symbol.alphanum
2006-07-25 haftmann 2006-07-25 improvements for lazy code generation
2006-07-25 haftmann 2006-07-25 fixed typo
2006-07-25 haftmann 2006-07-25 added code generator serialization for Char
2006-07-25 haftmann 2006-07-25 added notes on class_package.ML and codegen_package.ML
2006-07-23 haftmann 2006-07-23 small adjustments
2006-07-23 haftmann 2006-07-23 fixed bug for serialization for uminus on ints
2006-07-23 haftmann 2006-07-23 small improvement in serialization for wfrec
2006-07-23 haftmann 2006-07-23 added structure HOList
2006-07-23 haftmann 2006-07-23 major simplifications for integers
2006-07-23 haftmann 2006-07-23 tactic for prove_instance_arity now gets definition theorems as arguments
2006-07-21 haftmann 2006-07-21 added term_of_string function
2006-07-21 haftmann 2006-07-21 simplification for code generation for Integers
2006-07-21 haftmann 2006-07-21 adaption to argument change in primrec_package
2006-07-21 haftmann 2006-07-21 adaption to changes in class_package
2006-07-21 haftmann 2006-07-21 hooks now take string list as arguments (mutual datatypes); some nice combinators in datatype_codegen
2006-07-21 haftmann 2006-07-21 exported equation transformator
2006-07-21 haftmann 2006-07-21 class package and codegen refinements
2006-07-21 haftmann 2006-07-21 added give_names and alphanum
2006-07-21 berghofe 2006-07-21 Some cases in "case ... of ..." expressions may now be omitted (internally, these cases are assigned the "undefined" value).
2006-07-21 berghofe 2006-07-21 - Added new "undefined" constant - normalization_conv no longer expects term to have form "Trueprop ..."
2006-07-20 wenzelm 2006-07-20 removed Variable.monomorphic;
2006-07-20 webertj 2006-07-20 comments fixed, member function renamed
2006-07-19 ballarin 2006-07-19 Change to algebra method.
2006-07-19 ballarin 2006-07-19 Reimplemented algebra method; now controlled by attribute.
2006-07-19 ballarin 2006-07-19 Strict dfs traversal of imported and registered identifiers.
2006-07-19 haftmann 2006-07-19 added map_default, internal restructuring
2006-07-19 wenzelm 2006-07-19 export is_tid;
2006-07-19 wenzelm 2006-07-19 thm_of_proof: improved generation of variables;
2006-07-19 wenzelm 2006-07-19 Sign.infer_types: Name.context; FactIndex.add_local: simplified interface; Variable.constraints_of;
2006-07-19 wenzelm 2006-07-19 reorganize declarations (more efficient); renamed rename_wrt to variant_frees (avoid confusion with Term.rename_wrt_term, which reverses the result); tuned;
2006-07-19 wenzelm 2006-07-19 Name.context for used'';
2006-07-19 wenzelm 2006-07-19 added variant_frees; tuned;
2006-07-19 wenzelm 2006-07-19 tuned;
2006-07-19 wenzelm 2006-07-19 export make_context, is_declared;
2006-07-19 wenzelm 2006-07-19 prove: Variable.declare_internal (more efficient);
2006-07-19 wenzelm 2006-07-19 add_local: simplified interface, all frees are known'';
2006-07-19 wenzelm 2006-07-19 Sign.infer_types: Name.context;
2006-07-19 wenzelm 2006-07-19 renamed Variable.rename_wrt to Variable.variant_frees;
2006-07-19 paulson 2006-07-19 Fixed the bugs introduced by the last commit! Output is now *identical* to that produced by the old version, based on a-lists.
2006-07-19 webertj 2006-07-19 MiniSat proof trace format changed; MiniSat is now expected to produce a proof also for "trivial" problems
2006-07-18 wenzelm 2006-07-18 thm_of_proof: tuned Name operations;
2006-07-18 wenzelm 2006-07-18 print_statement: tuned Variable operations;
2006-07-18 wenzelm 2006-07-18 added newly_fixed, focus; removed monomorphic; tuned;
2006-07-18 wenzelm 2006-07-18 added declare_term_names; tuned;
2006-07-18 wenzelm 2006-07-18 fold_proof_terms: canonical arguments; removed obsolete add_prf_names, add_prf_tfree_names, add_prf_tvar_ixns;
2006-07-18 wenzelm 2006-07-18 Term.declare_term_names;
2006-07-18 berghofe 2006-07-18 Started implementing uniqueness proof for recursion combinator (still unfinished).
2006-07-18 webertj 2006-07-18 typo (theorerms) fixed
2006-07-18 webertj 2006-07-18 typo (theorerms) fixed
2006-07-18 haftmann 2006-07-18 AList.join now with 'DUP' exception