isabellebody: \par at begin/end;

auto update

first version of Advanced Inductive Defs section

x-symbol support for Pi, Sigma, -->, : (membership) note that "lam" is displayed as TWO lambda-symbols

new Main.thy as in HOL, ZF

added read_terms, read_props (simulataneous type-inference);

tuned statement args;

tuned IsarThy.theorem_i;

added students

Removed > and >=

Removed > and >= again.

quot_cond_definition;

simplified induction;

updated;