src/ZF/Bool.thy
2002-07-09 paulson 2002-07-09 better document preparation
2002-07-02 paulson 2002-07-02 Tidying and introduction of various new theorems
2002-06-22 paulson 2002-06-22 converted Bool, Trancl, Rel to Isar format
2002-06-18 paulson 2002-06-18 tidying
2000-08-10 paulson 2000-08-10 installation of cancellation simprocs for the integers
1997-01-23 wenzelm 1997-01-23 turned some consts into syntax;
1997-01-03 paulson 1997-01-03 Implicit simpsets and clasets for FOL and ZF
1996-03-29 paulson 1996-03-29 Mended indentation
1996-02-06 clasohm 1996-02-06 expanded tabs
1995-12-09 clasohm 1995-12-09 removed quotes from consts and syntax sections
1994-12-23 lcp 1994-12-23 Re-indented declarations; declared the number 2
1994-12-16 lcp 1994-12-16 put quotation marks around constant "and" because it is a keyword for inductive definitions!!
1994-11-29 lcp 1994-11-29 replaced "rules" by "defs"
1993-11-16 clasohm 1993-11-16 made pseudo theories for all ML files; documented dependencies between all thy and ML files
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-16 clasohm 1993-09-16 Initial revision