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;

overloading: tuned signature;

Instead of raising an exception, pred_set_conv now ignores conversion rules that would cause a clash. This allows multiple interpretations of locales containing inductive sets.

fix broken syntax translations

use ML antiquotations