ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext ex/prop-log/hyps_thms_if: split up the fast_tac call for more speed called expandshort

ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext domrange/image_subset,vimage_subset: deleted needless premise! misc: This slightly simplifies two proofs in Schroeder-Bernstein Theorem ind-syntax/rule_concl: recoded to avoid exceptions intr-elim: now checks conclusions of introduction rules func/fun_disjoint_Un: now uses ex_ex1I list-fn/hd,tl,drop: new simpdata/bquant_simps: new list/list_case_type: restored! bool.thy: changed 1 from a "def" to a translation Removed occurreces of one_def in bool.ML, nat.ML, univ.ML, ex/integ.ML nat/succ_less_induct: new induction principle arith/add_mono: new results about monotonicity simpdata/mem_simps: removed the ones for succ and cons; added succI1, consI2 to ZF_ss upair/succ_iff: new, for use with simp_tac (cons_iff already existed) ordinal/Ord_0_in_succ: renamed from Ord_0_mem_succ nat/nat_0_in_succ: new ex/prop-log/hyps_thms_if: split up the fast_tac call for more speed

ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext domrange/image_subset,vimage_subset: deleted needless premise! misc: This slightly simplifies two proofs in Schroeder-Bernstein Theorem ind-syntax/rule_concl: recoded to avoid exceptions intr-elim: now checks conclusions of introduction rules func/fun_disjoint_Un: now uses ex_ex1I list-fn/hd,tl,drop: new simpdata/bquant_simps: new list/list_case_type: restored! bool.thy: changed 1 from a "def" to a translation Removed occurreces of one_def in bool.ML, nat.ML, univ.ML, ex/integ.ML nat/succ_less_induct: new induction principle arith/add_mono: new results about monotonicity simpdata/mem_simps: removed the ones for succ and cons; added succI1, consI2 to ZF_ss upair/succ_iff: new, for use with simp_tac (cons_iff already existed) ordinal/Ord_0_in_succ: renamed from Ord_0_mem_succ nat/nat_0_in_succ: new ex/prop-log/hyps_thms_if: split up the fast_tac call for more speed

Added example from Avron: Gentzen-Type Systems, Resolution and Tableaux, JAR 10

Added ex_ex1I: new introduction rule for the EX! quantifier.

Added MRS, MRL from ZF/ROOT.ML. These support forward proof, resolving a rule's premises against a list of other proofs.

This commit should not have been necessary. For some reason, the previous commit did not update genrec.ML. There were still occurrences of SIMP_TAC. Was the commit perhaps interrupted??

make-all now has set +e so that New Jersey runs will continue even if some logic fails. change_simp added to help change to new simplifier.

Installation of new simplfier. Previously appeared to set up the old simplifier to rewrite with the partial ordering [=, something not possible with the new simplifier. But such rewriting appears not to have actually been used, and there were few complications. In terms.ML setloop was used to avoid infinite rewriting with the letrec rule. Congruence rules were deleted, and an occasional SIMP_TAC had to become asm_simp_tac.

Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is particularly delicate. There is a variable renaming problem in ramsey.ML/pigeon2_lemma. In some cases, rewriting by typechecking rules had to be replaced by setsolver type_auto_tac... because only the solver can instantiate variables.