"The" now a binder, removed translation; improved encoding and translations of tuples; added parse rules for -> and *, removed ndependent_tr;

removed ndependent_tr (no longer needed, use _K);

*** empty log message ***

*** empty log message ***

fixed comment;

added parse rule for "<*>"; removed ndependent_tr;

@List: replaced "args" by "is";

*** empty log message ***

added cons, rcons, last_elem, sort_strings, take_suffix; improved tack_on;

added raise_type: string -> typ list -> term list -> 'a; added raise_term: string -> term list -> 'a;

"The error/exception above ...": errorneous goal now quoted;

used ~: for "not in"

added ~: for "not in"

examples now use ~= for "not equals"

ifol.thy: added ~= for "not equals"

changed filenames to lower case name of theory the file contains (only one theory per file, therefore llist.ML has been split)

rename list-fn to listfn

changed "list-fn" to "listfn"

tctical/dummy_quant_rl: specifies type prop to avoid the type variable ?'a from occurring -- which sometimes caused SELECT_GOAL to fail

Retrying yet again after network problems

Modification of examples for the new operators, < and le.

Retry of the previous commit (network outage)

Retry of the previous commit (network outage)

ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many changes epsilon,arith: many changes ordinal/succ_mem_succI/E: deleted; use succ_leI/E nat/nat_0_in_succ: deleted; use nat_0_le univ/Vset_rankI: deleted; use VsetI

ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many changes epsilon,arith: many changes ordinal/succ_mem_succI/E: deleted; use succ_leI/E nat/nat_0_in_succ: deleted; use nat_0_le univ/Vset_rankI: deleted; use VsetI

added functions that operate on filenames: split_filename (originally located in Pure/read.ML), tack_on, remove_ext

replaced id by idt; added parse rules for --> and *; removed ndependent_tr;

added parse rules for -> and *; removed ndependent_tr;

replaced id by idt; added parse rule for ->; removed ndependent_tr;

Pure/Thy/syntax.ML removed {parse,print}_{pre,post}_proc; removed 'val ax = ..';

Pure/ROOT.ML cleaned comments; removed extraneous 'print_depth 1'; replaced Basic_Syntax by BasicSyntax added 'use "install_pp.ML"'; Pure/README fixed comments; Pure/POLY.ML Pure/NJ.ML make_pp: added fbrk; Pure/install_pp.ML replaced "Ast" by "Syntax"; Pure/sign.ML added 'quote' to some error msgs;

lots of internal cleaning and tuning; removed {parse,print}_{pre,post}_proc; new lexer: now human readable due to scanner combinators; new parser installed, but still inactive (due to grammar ambiguities); added Syntax.test_read; typ_of_term: sorts now made distinct and sorted; mixfix: added forced line breaks (//); PROP now printed before subterm of type prop with non-const head;

asm_full_simp_tac now fails when applied to a state w/o subgoals.

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.

Installation of new simplifier for ZF. Deleted all congruence rules not involving local assumptions. NB the congruence rules for Sigma and Pi (dependent type constructions) cause difficulties and are not used by default.

test commit

added header

defined local addcongs

moved use of Thy/ROOT.ML to end of file because Thy/read.ML needs Thm

changed addcongs to addeqcongs in simplifier.ML

Initial revision