2015-07-23 wenzelm 2015-07-23 isabelle update_cartouches;
2014-11-02 wenzelm 2014-11-02 modernized header;
2012-03-06 paulson 2012-03-06 Using mathematical notation for <-> and cardinal arithmetic
2012-03-06 paulson 2012-03-06 mathematical symbols instead of ASCII
2012-03-01 paulson 2012-03-01 Removal of obsolete ML bindings
2011-11-20 wenzelm 2011-11-20 eliminated obsolete "standard";
2011-02-18 wenzelm 2011-02-18 more precise headers;
2010-09-06 wenzelm 2010-09-06 more antiquotations;
2010-03-13 wenzelm 2010-03-13 removed old CVS Ids; tuned headers;
2007-10-07 wenzelm 2007-10-07 modernized specifications; removed legacy ML bindings;
2007-10-07 wenzelm 2007-10-07 replaced some 'translations' by 'abbreviation';
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2002-07-14 paulson 2002-07-14 improved presentation markup
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