moved meta_fun_cong lemma into ML-file; tuned

merged

adapted Function_Lib (cf. b8cdd3d73022);

configuration flag "partials"

renamed auto_term.ML -> relation.ML

function package: more standard names for structures and files

renamed FundefDatatype -> Function_Fun

maintain position of formal entities via name space;

maintain explicit name space kind; export Name_Space.the_entry; tuned messages;

renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;

eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already; simplified messages;

eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already; fully authentic merge;

eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;

maintain abstract entry, with position, identity etc.; declare/define: explicit indication of strictness; merge_tables/join_tables: disallow duplicates based on entry identity;

tuned message;

import theory Nat here, which avoids duplicate definition of datatype_realizers (and thus allows to maintain fully authentic fact table);

markup for formal entities, with "def" or "ref" occurrences;

handle Sorts.CLASS_ERROR instead of arbitrary exceptions;

reactivated isatest on macbroy6 -- 3h later to avoid overlap with backup daemon;

merged

turned off old quickcheck

pat_completeness gets its own file

ignore error messages produced by ATPs

merged

renamed f_inv_onto_f to f_inv_into_f (cf. 764547b68538)

restored accidentally deleted submultiset

multiset operations with canonical argument order

arg_types_of auxiliary function; using multiset operations

merged

close thm derivations explicitly