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;

use inverse, divide from basic HOL;

norm_hhf_tac;

rewrite_goal_tac moved to tactic.ML;

added rewrite_goal_tac;

added certify_tycon, certify_tyabbr, certify_const;

has_meta_prems: include "==";

store_standard_thm "norm_hhf_eq";

proper theory context for mesontest2;

inductive_rulify2 accomodates malformed induction rules;

Sign.certify_tycon, Sign.certify_const;