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

Fix a duplicate abbreviation || in etc/symbols.

made SML/NJ happy;

updated session name;

renamed f_inv_onto_f to f_inv_into_f (cf. 764547b68538);

merged

merged

merged

use plain Scan.repeat (NB: Scan.bulk is for cascading sources -- mostly interna use);

merged