System shell processes, with static input/output and propagation of interrupts.

added General/system_process.ML;

added lemma lists {normalize,succ,pred,minus,add,mult}_bin_simps

added lemma lists {normalize,succ,pred,minus,add,mult}_bin_simps

support for managed external processes;

more lemmas

<= and < on nat no longer depend on wellfounded relations

moved *_reorient lemmas here

tuned names;

syntax error: suppress expected categories altogether;

expected syntax categories: reduced duplication, report minimal priorities only;

Fixed typing problem that caused instantiation of induct_aux_rec to go wrong.

make_meta_clause bugfix: now works for higher-order clauses like LeastI_ex

fixed record pretty printing

using integers for pattern matching

tuned whitespace

more abstract lemmas

fix spelling

imports Main;

removed unnecessary theory qualifiers;

simultaneous use_thys;

added Id;

Made theory names in ZF disjoint from HOL theory names to allow loading both developments in a single session (but not merge them).

tuned proofs and comments

tuned spaces;

tuned default position;

added default_properties;

added position_properties;

maintain default position;

overloading: reduced code redundancy, no xstrings here;