Mon, 04 Oct 1993 15:38:02 +0100 Pure/Thy/syntax.ML
wenzelm [Mon, 04 Oct 1993 15:38:02 +0100] rev 20
Pure/Thy/syntax.ML removed {parse,print}_{pre,post}_proc; removed 'val ax = ..';
Mon, 04 Oct 1993 15:36:31 +0100 Pure/ROOT.ML
wenzelm [Mon, 04 Oct 1993 15:36:31 +0100] rev 19
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;
Mon, 04 Oct 1993 15:30:49 +0100 lots of internal cleaning and tuning;
wenzelm [Mon, 04 Oct 1993 15:30:49 +0100] rev 18
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;
Fri, 01 Oct 1993 13:26:22 +0100 asm_full_simp_tac now fails when applied to a state w/o subgoals.
nipkow [Fri, 01 Oct 1993 13:26:22 +0100] rev 17
asm_full_simp_tac now fails when applied to a state w/o subgoals.
Thu, 30 Sep 1993 10:54:01 +0100 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp [Thu, 30 Sep 1993 10:54:01 +0100] rev 16
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
Thu, 30 Sep 1993 10:26:38 +0100 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp [Thu, 30 Sep 1993 10:26:38 +0100] rev 15
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
Thu, 30 Sep 1993 10:10:21 +0100 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp [Thu, 30 Sep 1993 10:10:21 +0100] rev 14
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
Fri, 24 Sep 1993 11:27:15 +0200 Added example from Avron: Gentzen-Type Systems, Resolution and Tableaux, JAR 10
lcp [Fri, 24 Sep 1993 11:27:15 +0200] rev 13
Added example from Avron: Gentzen-Type Systems, Resolution and Tableaux, JAR 10
Fri, 24 Sep 1993 11:13:55 +0200 Added ex_ex1I: new introduction rule for the EX! quantifier.
lcp [Fri, 24 Sep 1993 11:13:55 +0200] rev 12
Added ex_ex1I: new introduction rule for the EX! quantifier.
Fri, 24 Sep 1993 10:52:55 +0200 Added MRS, MRL from ZF/ROOT.ML. These support forward proof, resolving a
lcp [Fri, 24 Sep 1993 10:52:55 +0200] rev 11
Added MRS, MRL from ZF/ROOT.ML. These support forward proof, resolving a rule's premises against a list of other proofs.
Tue, 21 Sep 1993 11:16:19 +0200 This commit should not have been necessary. For some reason, the previous
lcp [Tue, 21 Sep 1993 11:16:19 +0200] rev 10
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??
Mon, 20 Sep 1993 18:39:45 +0200 make-all now has set +e so that New Jersey runs will continue even if some
lcp [Mon, 20 Sep 1993 18:39:45 +0200] rev 9
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.
Mon, 20 Sep 1993 17:02:11 +0200 Installation of new simplfier. Previously appeared to set up the old
lcp [Mon, 20 Sep 1993 17:02:11 +0200] rev 8
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.
Fri, 17 Sep 1993 16:52:10 +0200 Installation of new simplifier for ZF/ex. The hom_ss example in misc.ML is
lcp [Fri, 17 Sep 1993 16:52:10 +0200] rev 7
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.
Fri, 17 Sep 1993 16:16:38 +0200 Installation of new simplifier for ZF. Deleted all congruence rules not
lcp [Fri, 17 Sep 1993 16:16:38 +0200] rev 6
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.
Fri, 17 Sep 1993 12:53:53 +0200 test commit
lcp [Fri, 17 Sep 1993 12:53:53 +0200] rev 5
test commit
Thu, 16 Sep 1993 17:41:10 +0200 added header
nipkow [Thu, 16 Sep 1993 17:41:10 +0200] rev 4
added header
Thu, 16 Sep 1993 16:55:17 +0200 defined local addcongs
nipkow [Thu, 16 Sep 1993 16:55:17 +0200] rev 3
defined local addcongs
Thu, 16 Sep 1993 16:25:32 +0200 moved use of Thy/ROOT.ML to end of file because Thy/read.ML needs Thm
clasohm [Thu, 16 Sep 1993 16:25:32 +0200] rev 2
moved use of Thy/ROOT.ML to end of file because Thy/read.ML needs Thm
Thu, 16 Sep 1993 14:21:44 +0200 changed addcongs to addeqcongs in simplifier.ML
nipkow [Thu, 16 Sep 1993 14:21:44 +0200] rev 1
changed addcongs to addeqcongs in simplifier.ML
Thu, 16 Sep 1993 12:20:38 +0200 Initial revision
clasohm [Thu, 16 Sep 1993 12:20:38 +0200] rev 0
Initial revision
(0) +30 +50 +100 +300 +1000 +3000 +10000 +30000 tip