Lemma "fundef_default_value" uses predicate instead of set.

The function package declares the [code] attribute automatically again.

exported mk_base_funs for use by size-change tools

ATP linkup now generates "new TPTP" rather than "old TPTP"

more careful declaration of "inducts";

tuned;

prefer Proof.context over Context.generic;

prefer Proof.context over Context.generic; tuned;

tuned proofs;

Accept URLs of form file:/home... also.

prefer antiquotations over LaTeX macros;

updated;

renamed Args.Name to Args.Text;

uniform interface for type_syntax/term_syntax/declaration, dependent on morphism; tuned some morphisms;

uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;

Morphism.thm_morphism;

renamed Name value to Text, which is *not* a name in terms of morphisms;

removed obsolete alphanum;

str_of_char: improved output of non-printables;

added head_name_of;

added name/var/typ/term/thm_morphism; removed transfer;

declarations: pass morphism (dummy);

added ISABELLE_IDENTIFIER; removed THIS_IS_ISABELLE_BUILD magic;

ISABELLE_PATH/OUTPUT: append ISABELLE_IDENTIFIER if derived from ISABELLE_HOME_USER;

fixed some typos

tuned the proof of the strong induction principle

typo in comment fixed

Add retractfile to supported pgip commands