Plain, Main form meeting points in import hierarchy

added lemma abs_sng

nat is a bot instance

slightly adapted towards more uniformity with div/mod on nat

Reflection.thy now in HOL/Library

more robust treatment of SwingUtilities.isEventDispatchThread;

annotate shared vars as @volatile;

updated generated file;

added label;

plain non-dependent types;

turned IsarDocument into trait for IsabelleProcess;

HOL_USEDIR_OPTIONS: -Q false, giving up parallel proofs for now due to memory shortage;

thm_proof: recovered single-threaded version;

merged

recovered example types from WordMain.thy;

merged

added share_common_data -- reduces heap space, but takes long;

use https;

thm_proof: replaced lazy by composed futures;

proof_body: turned lazy into future -- ensures that body is fulfilled eventually, without explicit force;

explicit constraints

entry point for Word library now named Word

fixed reading of class specs: declare class operations in context

stripped Id

streamlined definitions, executable equality

tuned header

entry point for Word library now named Word

correct proof of assm_intro rule

sorted_take, sorted_drop

merged

fixed fixme

avoiding misleading name duplicate

lemmas dom_const, dom_if

merged

moved all output to watcher-thread

be more liberal with selected code statements

making SMLNJ happy

tuned signature;

binding replaces Binding.T

binding replaces bstring

simplified handling of base sort, dropped axclass

dropped print_interps

binding replaces bstring

merged

allow empty class specs

changed import hierarchy

no base sort in class import

updated generated files;

removed Ids;

eliminated obsolete var morphism;

eliminated obsolete var morphism; tuned;

eliminated obsolete var morphism; simplified map_ctxt: just one version, without var; removed obsolete params_of, prems_of, facts_of; removed obsolete rename operations; tuned;

merged

tuned whitespace;

merged

removed vampire-wrapper (remote-script covers that)