2000-11-18 ago wenzelm default_intro_classes_tac: Tactic.distinct_subgoals_tac;
2000-11-18 ago wenzelm axclass ordered_ring;
2000-11-18 ago wenzelm quot_cond_function: simplified, support conditional definition;
2000-11-18 ago wenzelm abs_eq_0: #0 instead of 0;
2000-11-18 ago wenzelm symbol syntax for "abs";
2000-11-18 ago wenzelm added axclass ordered_field;
2000-11-17 ago wenzelm check result: Envir.beta_norm;
2000-11-17 ago wenzelm Envir.beta_norm;
2000-11-17 ago wenzelm added beta_norm;
2000-11-17 ago wenzelm tuned;
2000-11-17 ago wenzelm removed quot_cond_function1, quot_function1;
2000-11-17 ago wenzelm UNIV_witness;
2000-11-17 ago wenzelm Ring_and_Field;
2000-11-17 ago wenzelm Library/Ring_and_Field.thy;
2000-11-16 ago bauerg rings and fields;
2000-11-16 ago wenzelm Proof.assert_forward;
2000-11-16 ago wenzelm added not_equiv_sym, not_equiv_trans1/2;
2000-11-16 ago wenzelm added abs_mult, abs_eq_0, square_nonzero;
2000-11-16 ago paulson ground terms section: new intro
2000-11-16 ago paulson CTT
2000-11-15 ago wenzelm separate rules for function/operation definitions;
2000-11-15 ago wenzelm renamed integ_le_less to int_le_less;
2000-11-15 ago wenzelm updated;
2000-11-15 ago wenzelm isabellebody: \par at begin/end;
2000-11-14 ago paulson auto update
2000-11-14 ago paulson first version of Advanced Inductive Defs section
2000-11-14 ago paulson x-symbol support for Pi, Sigma, -->, : (membership)
2000-11-14 ago paulson new Main.thy as in HOL, ZF
2000-11-13 ago wenzelm added read_terms, read_props (simulataneous type-inference);
2000-11-13 ago wenzelm tuned statement args;
2000-11-13 ago wenzelm tuned IsarThy.theorem_i;
2000-11-13 ago kleing added students
2000-11-13 ago nipkow Removed > and >=
2000-11-13 ago nipkow Removed > and >= again.
2000-11-12 ago wenzelm quot_cond_definition;
2000-11-12 ago wenzelm simplified induction;
2000-11-12 ago wenzelm updated;
2000-11-12 ago wenzelm "induct" method: handle proper rules;
2000-11-12 ago wenzelm removed warning for "stripped" option;
2000-11-12 ago wenzelm removed junk;
2000-11-12 ago wenzelm Syntax.pure_appl_syntax declared as output syntax for theory ProtoPure;
2000-11-10 ago wenzelm * added overloaded operations "inverse" and "divide" (infix "/");
2000-11-10 ago wenzelm int_distrib;
2000-11-10 ago wenzelm nat_distrib;
2000-11-10 ago wenzelm hide_space(_i): use Sign.certify_tycon, Sign.certify_tyabbr, Sign.certify_const;
2000-11-10 ago wenzelm tuned;
2000-11-10 ago wenzelm use inverse, divide from basic HOL;
2000-11-10 ago wenzelm norm_hhf_tac;
2000-11-10 ago wenzelm rewrite_goal_tac moved to tactic.ML;
2000-11-10 ago wenzelm added rewrite_goal_tac;
2000-11-10 ago wenzelm added certify_tycon, certify_tyabbr, certify_const;
2000-11-10 ago wenzelm has_meta_prems: include "==";
2000-11-10 ago wenzelm store_standard_thm "norm_hhf_eq";
2000-11-10 ago wenzelm proper theory context for mesontest2;
2000-11-10 ago wenzelm inductive_rulify2 accomodates malformed induction rules;
2000-11-10 ago wenzelm Sign.certify_tycon, Sign.certify_const;
2000-11-10 ago wenzelm improved cong_definition theorems;
2000-11-10 ago wenzelm simplified induction;
2000-11-10 ago wenzelm added axclass power (from HOL.thy);
2000-11-10 ago wenzelm simplified atomize;