1993-10-17 clasohm 1993-10-17 renamed: terms.* to term.*, types.* to type.*, wf.* to wfd.*
1993-10-15 clasohm 1993-10-15 file_info now returns a string that does not contain the path/filename (so the string doesn't change when the relative path does)
1993-10-15 wenzelm 1993-10-15 added parser.ML, install_pp.ML
1993-10-15 lcp 1993-10-15 ZF/ex/tf/tree,forest_unfold: streamlined the proofs Updated other inductive def examples as per changes in the package.
1993-10-15 lcp 1993-10-15 ZF/ind-syntax/refl_thin: new ZF/intr-elim: added Pair_neq_0, succ_neq_0, refl_thin to simplify case rules ZF/sum/Inl_iff, etc.: tidied and proved using simp_tac ZF/qpair/QInl_iff, etc.: tidied and proved using simp_tac ZF/datatype,intr_elim: replaced the undirectional use of sum_univ RS subsetD by dresolve_tac InlD,InrD and etac PartE
1993-10-15 lcp 1993-10-15 classical/swap_res_tac: recoded to allow backtracking
1993-10-12 nipkow 1993-10-12 Added gen_all to simpdata.ML.
1993-10-11 clasohm 1993-10-11 renamed ordinal.thy to ord.thy
1993-10-11 clasohm 1993-10-11 renamed ordinal.ML to ord.ML
1993-10-11 clasohm 1993-10-11 renamed ordinal.* to ord.*
1993-10-11 wenzelm 1993-10-11 "The" now a binder, removed translation; improved encoding and translations of tuples; added parse rules for -> and *, removed ndependent_tr;
1993-10-11 wenzelm 1993-10-11 removed ndependent_tr (no longer needed, use _K);
1993-10-11 wenzelm 1993-10-11 *** empty log message ***
1993-10-08 wenzelm 1993-10-08 *** empty log message ***
1993-10-08 wenzelm 1993-10-08 fixed comment;
1993-10-08 wenzelm 1993-10-08 added parse rule for "<*>"; removed ndependent_tr;
1993-10-08 wenzelm 1993-10-08 @List: replaced "args" by "is";
1993-10-08 wenzelm 1993-10-08 *** empty log message ***
1993-10-08 wenzelm 1993-10-08 added cons, rcons, last_elem, sort_strings, take_suffix; improved tack_on;
1993-10-08 wenzelm 1993-10-08 added raise_type: string -> typ list -> term list -> 'a; added raise_term: string -> term list -> 'a;
1993-10-08 wenzelm 1993-10-08 "The error/exception above ...": errorneous goal now quoted;
1993-10-07 lcp 1993-10-07 used ~: for "not in"
1993-10-07 lcp 1993-10-07 added ~: for "not in"
1993-10-07 lcp 1993-10-07 examples now use ~= for "not equals"
1993-10-07 lcp 1993-10-07 ifol.thy: added ~= for "not equals"
1993-10-06 clasohm 1993-10-06 changed filenames to lower case name of theory the file contains (only one theory per file, therefore llist.ML has been split)
1993-10-06 clasohm 1993-10-06 rename list-fn to listfn
1993-10-06 clasohm 1993-10-06 changed "list-fn" to "listfn"
1993-10-06 lcp 1993-10-06 tctical/dummy_quant_rl: specifies type prop to avoid the type variable ?'a from occurring -- which sometimes caused SELECT_GOAL to fail
1993-10-06 lcp 1993-10-06 Retrying yet again after network problems
1993-10-05 lcp 1993-10-05 Modification of examples for the new operators, < and le.
1993-10-05 lcp 1993-10-05 Retry of the previous commit (network outage)
1993-10-05 lcp 1993-10-05 Retry of the previous commit (network outage)
1993-10-05 lcp 1993-10-05 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
1993-10-05 lcp 1993-10-05 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
1993-10-05 clasohm 1993-10-05 added functions that operate on filenames: split_filename (originally located in Pure/read.ML), tack_on, remove_ext
1993-10-04 wenzelm 1993-10-04 replaced id by idt; added parse rules for --> and *; removed ndependent_tr;
1993-10-04 wenzelm 1993-10-04 added parse rules for -> and *; removed ndependent_tr;
1993-10-04 wenzelm 1993-10-04 replaced id by idt; added parse rule for ->; removed ndependent_tr;
1993-10-04 wenzelm 1993-10-04 Pure/Thy/syntax.ML removed {parse,print}_{pre,post}_proc; removed 'val ax = ..';
1993-10-04 wenzelm 1993-10-04 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;
1993-10-04 wenzelm 1993-10-04 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;
1993-10-01 nipkow 1993-10-01 asm_full_simp_tac now fails when applied to a state w/o subgoals.
1993-09-30 lcp 1993-09-30 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
1993-09-30 lcp 1993-09-30 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
1993-09-30 lcp 1993-09-30 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
1993-09-24 lcp 1993-09-24 Added example from Avron: Gentzen-Type Systems, Resolution and Tableaux, JAR 10
1993-09-24 lcp 1993-09-24 Added ex_ex1I: new introduction rule for the EX! quantifier.
1993-09-24 lcp 1993-09-24 Added MRS, MRL from ZF/ROOT.ML. These support forward proof, resolving a rule's premises against a list of other proofs.
1993-09-21 lcp 1993-09-21 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??
1993-09-20 lcp 1993-09-20 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.
1993-09-20 lcp 1993-09-20 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.
1993-09-17 lcp 1993-09-17 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.
1993-09-17 lcp 1993-09-17 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.
1993-09-17 lcp 1993-09-17 test commit
1993-09-16 nipkow 1993-09-16 added header
1993-09-16 nipkow 1993-09-16 defined local addcongs
1993-09-16 clasohm 1993-09-16 moved use of Thy/ROOT.ML to end of file because Thy/read.ML needs Thm
1993-09-16 nipkow 1993-09-16 changed addcongs to addeqcongs in simplifier.ML
1993-09-16 clasohm 1993-09-16 Initial revision