added raw_string_of_sort/typ/term;

simple substructure test for typargs (independent type constructors);

tuned;

string_of_option tuned

* Isar: removed obsolete 'concl is' patterns.

removed 'concl is' pattern;

removed 'concl is' patterns;

tuned;

function-package: Changed record usage to make sml/nj happy...

get rid of 'concl is';

more robust pretty_term_typ, using well-typed parse tree representation;

replaced find_paths by irreducible_paths, i.e. produce paths within a Hasse diagram;

replaced Sorts.DOMAIN by general Sorts.CLASS_ERROR; add_types etc.: reject qualified dummy types -- prevents users from messing up some internal conventions;

added class_error and exception CLASS_ERROR (supercedes DOMAIN); clarified of_class_derivation; tuned witness_sorts;

added syntax for _type_constraint_;

extern_early: improved handling of undeclared constants;

replaced Graph.find_paths by Graph.irreducible_paths;

of_sort: explicit cache value; simplified internal representation of instances;

axiomatization;

* Library: theory Accessible_Part has been move to main HOL.

Theory.definitions_of;

added definitions_of;

specifications_of: more detailed information; tuned;

Added small example theory for new function package.

string_of_... functions added

added the lemma pt_fresh_bij2

added something

First usable version of the new function definition package (HOL/function_packake/...). Moved Accessible_Part.thy from Library to Main.