src/ZF/Arith.ML
1999-01-29 paulson 1999-01-29 expandshort
1999-01-27 paulson 1999-01-27 new typechecking solver for the simplifier
1999-01-07 paulson 1999-01-07 ZF: the natural numbers as a datatype
1999-01-07 paulson 1999-01-07 if-then-else syntax for ZF
1998-09-22 paulson 1998-09-22 tidying
1998-09-18 paulson 1998-09-18 new theorem less_imp_Suc_add
1998-08-19 paulson 1998-08-19 new theorem zero_less_diff
1998-08-17 paulson 1998-08-17 Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy contains fewer theorems than before
1998-07-15 paulson 1998-07-15 More tidying and removal of "\!\!... from Goal commands
1998-07-13 paulson 1998-07-13 Huge tidy-up: removal of leading \!\! addsplits split_tac[split_if] now default nat_succI now included by default
1998-07-02 paulson 1998-07-02 Renamed expand_if to split_if and setloop split_tac to addsplits, as in HOL
1998-06-22 wenzelm 1998-06-22 isatool fixgoal;
1998-04-28 paulson 1998-04-28 new thm mult_lt_mono1
1997-11-03 wenzelm 1997-11-03 isatool fixclasimp;
1997-10-10 wenzelm 1997-10-10 fixed dots;
1997-09-29 paulson 1997-09-29 Much tidying including step_tac -> clarify_tac or safe_tac; sometimes used qed_spec_mp
1997-05-15 oheimb 1997-05-15 renamed unsafe_addss to addss
1997-04-23 paulson 1997-04-23 Conversion to use blast_tac
1997-02-15 oheimb 1997-02-15 reflecting my recent changes of the simplifier and classical reasoner
1997-01-08 paulson 1997-01-08 Removal of sum_cs and eq_cs
1997-01-03 paulson 1997-01-03 Implicit simpsets and clasets for FOL and ZF
1996-09-26 paulson 1996-09-26 Ran expandshort; used stac instead of ssubst
1996-06-13 paulson 1996-06-13 New example of GCDs and divides relation
1996-05-01 paulson 1996-05-01 tidied some proofs
1996-03-28 paulson 1996-03-28 Ran expandshort
1996-03-26 paulson 1996-03-26 New lemmas for Mutilated Checkerboard
1996-01-30 clasohm 1996-01-30 expanded tabs
1994-12-07 clasohm 1994-12-07 added qed and qed_goal[w]
1994-06-23 lcp 1994-06-23 modifications for cardinal arithmetic
1994-06-21 lcp 1994-06-21 Addition of cardinals and order types, various tidying
1993-11-18 lcp 1993-11-18 Misc modifs such as expandshort
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-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-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-16 clasohm 1993-09-16 Initial revision