Conversion of "equal" to "=" for TSTP format; big tidy-up

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

PGIP: add retractfile. Be stricter in file open/close protocol.

replaced Args.map_values/Element.map_ctxt_values by general morphism application;

moved ML identifiers to structure ML_Syntax;

added morph_ctxt, morph_witness; removed ctxt/witness in favour of general morphisms;

replaced map_values by morph_values;

moved string_of_pair/list/option to structure ML_Syntax;

moved ML syntax operations to structure ML_Syntax;

Basic ML syntax operations.

Abstract morphisms on formal entities.

added morphism.ML, General/ml_syntax.ML;

renamed string_of_pair/list/option to ML_Syntax.str_of_pair/list/option;

removed dead code;

Add doccomment; rename litcomment -> doccomment

* settings: ML_IDENTIFIER includes the Isabelle version identifier;

Consolidation of code to "blacklist" unhelpful theorems, including record surjectivity properties

ML_IDENTIFIER includes Isabelle version;

add ISABELLE_VERSION to ML_IDENTIFIER, unless this is repository or build;

consts: ProofContext.set_stmt true -- avoids naming of local thms;

init: enter inner statement mode, which prevents local notes from being named internally;

more careful declaration of "intros" as Pure.intro;

Fix to local file URI syntax. Add first part of lexicalstructure command support.

completed class parameter handling in axclass.ML

added Isar syntax for adding parameters to axclasses

forced name prefix for class operations

example tuned

no explicit check for theory Nat

added code lemmas

does not import Hilber_Choice any longer

cleanup

incorporated structure HOList into HOLogic

dropped eq const