Removed wrong sentence (Simon Funke)

moved pprint functions to Isar/proof_display.ML;

Tactical operations depending on local subgoal structure.

moved pprint functions to Isar/proof_display.ML; added primitive add_assumes; tuned internal prems: no names;

export goal_tac (was internal refine_tac);

added Pure/subgoal.ML;

updated;

raw symbols: disallow dot to avoid confusion in NameSpace.unpack;

avoid Term.is_funtype;

avoid structure Char;

added variant_abs (from term.ML); tuned;

added find_free (from term.ML);

added is/to_ascii_lower/upper; tuned alphanum -- needs more work;

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;

tuned;

use Term.add_vars instead of obsolete term_varnames;

renamed add_term_varnames to Term.add_varnames (cf. Term.add_vars etc.);

tuned ML code;

renamed Term.variant_abs to Syntax.variant_abs;

Drule.merge_rules;

renamed Name.give_names to Name.names and moved Name.alphanum to Symbol.alphanum

improvements for lazy code generation

fixed typo

added code generator serialization for Char

added notes on class_package.ML and codegen_package.ML

small adjustments

fixed bug for serialization for uminus on ints

small improvement in serialization for wfrec

added structure HOList

major simplifications for integers

tactic for prove_instance_arity now gets definition theorems as arguments

added term_of_string function

simplification for code generation for Integers

adaption to argument change in primrec_package

adaption to changes in class_package

hooks now take string list as arguments (mutual datatypes); some nice combinators in datatype_codegen

exported equation transformator

class package and codegen refinements

added give_names and alphanum

Some cases in "case ... of ..." expressions may now be omitted (internally, these cases are assigned the "undefined" value).

- Added new "undefined" constant - normalization_conv no longer expects term to have form "Trueprop ..."

removed Variable.monomorphic;

comments fixed, member function renamed

Change to algebra method.

Reimplemented algebra method; now controlled by attribute.

Strict dfs traversal of imported and registered identifiers.

added map_default, internal restructuring

export is_tid;

thm_of_proof: improved generation of variables;

Sign.infer_types: Name.context; FactIndex.add_local: simplified interface; Variable.constraints_of;

reorganize declarations (more efficient); renamed rename_wrt to variant_frees (avoid confusion with Term.rename_wrt_term, which reverses the result); tuned;

Name.context for used'';

added variant_frees; tuned;

tuned;

export make_context, is_declared;

prove: Variable.declare_internal (more efficient);

add_local: simplified interface, all frees are known'';

Sign.infer_types: Name.context;

renamed Variable.rename_wrt to Variable.variant_frees;

Fixed the bugs introduced by the last commit! Output is now *identical* to that produced by the old version, based on a-lists.