2006-07-27 wenzelm 2006-07-27 read_def_cterms (legacy version): Consts.certify;
2006-07-27 wenzelm 2006-07-27 Assumption.assume;
2006-07-27 wenzelm 2006-07-27 moved Goal.norm_hhf(_protect) to meta_simplifier.ML (pervasive);
2006-07-27 wenzelm 2006-07-27 removed obsolete equal_abs_elim(_list);
2006-07-27 wenzelm 2006-07-27 removed obsolete pretty_thm_no_quote;
2006-07-27 wenzelm 2006-07-27 added Pure/assumption.ML;
2006-07-27 wenzelm 2006-07-27 moved basic assumption operations from structure ProofContext to Assumption;
2006-07-27 wenzelm 2006-07-27 tuned proofs;
2006-07-27 wenzelm 2006-07-27 Local assumptions, parameterized by export rules.
2006-07-26 wenzelm 2006-07-26 updated;
2006-07-26 wenzelm 2006-07-26 import(T): result includes fixed types/terms; focus: tuned interface;
2006-07-26 wenzelm 2006-07-26 focus: result record includes (fixed) schematic variables; SUBGOAL: disallow pending subgoals, more robust re-composition;
2006-07-26 wenzelm 2006-07-26 Variable.import(T): result includes fixed types/terms;
2006-07-26 webertj 2006-07-26 linear arithmetic splits certain operators (e.g. min, max, abs)
2006-07-26 haftmann 2006-07-26 added eval_term
2006-07-26 wenzelm 2006-07-26 updated;
2006-07-26 wenzelm 2006-07-26 fixed LaTeX problem;
2006-07-26 haftmann 2006-07-26 added eval_term
2006-07-26 nipkow 2006-07-26 Removed wrong sentence (Simon Funke)
2006-07-26 wenzelm 2006-07-26 moved pprint functions to Isar/proof_display.ML;
2006-07-26 wenzelm 2006-07-26 Tactical operations depending on local subgoal structure.
2006-07-26 wenzelm 2006-07-26 moved pprint functions to Isar/proof_display.ML; added primitive add_assumes; tuned internal prems: no names;
2006-07-26 wenzelm 2006-07-26 export goal_tac (was internal refine_tac);
2006-07-26 wenzelm 2006-07-26 added Pure/subgoal.ML;
2006-07-25 wenzelm 2006-07-25 updated;
2006-07-25 wenzelm 2006-07-25 raw symbols: disallow dot to avoid confusion in NameSpace.unpack;
2006-07-25 wenzelm 2006-07-25 avoid Term.is_funtype;
2006-07-25 wenzelm 2006-07-25 avoid structure Char;
2006-07-25 wenzelm 2006-07-25 added variant_abs (from term.ML); tuned;
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;