added not_equiv_sym, not_equiv_trans1/2; tuned;

added abs_mult, abs_eq_0, square_nonzero;

ground terms section: new intro

CTT

separate rules for function/operation definitions;

renamed integ_le_less to int_le_less;

updated;

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;

"induct" method: handle proper rules;

removed warning for "stripped" option;

removed junk;

Syntax.pure_appl_syntax declared as output syntax for theory ProtoPure;

* added overloaded operations "inverse" and "divide" (infix "/");

int_distrib;

nat_distrib;

hide_space(_i): use Sign.certify_tycon, Sign.certify_tyabbr, Sign.certify_const;

tuned;