src/FOL/FOL.thy
2011-04-22 wenzelm 2011-04-22 modernized Quantifier1 simproc setup;
2011-04-22 wenzelm 2011-04-22 clarified simpset setup; discontinued unused old-style FOL_css;
2011-02-23 noschinl 2011-02-23 setup case_product attribute in HOL and FOL
2011-02-18 wenzelm 2011-02-18 modernized specifications;
2010-12-20 wenzelm 2010-12-20 proper identifiers for consts and types;
2010-05-12 wenzelm 2010-05-12 modernized specifications;
2010-04-16 wenzelm 2010-04-16 replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
2010-01-30 berghofe 2010-01-30 Adapted to changes in setup of cases method.
2010-01-10 berghofe 2010-01-10 Adapted to changes in setup of induct method.
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2009-07-29 wenzelm 2009-07-29 removed old global get_claset/map_claset; added local get_claset/put_claset;
2009-07-24 wenzelm 2009-07-24 renamed functor BlastFun to Blast, require explicit theory; eliminated src/FOL/blastdata.ML;
2009-07-24 wenzelm 2009-07-24 renamed functor InductFun to Induct;
2009-07-09 wenzelm 2009-07-09 removed obsolete CVS Ids;
2009-03-16 wenzelm 2009-03-16 simplified method setup;
2008-11-20 wenzelm 2008-11-20 Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
2008-10-28 ballarin 2008-10-28 Removed 'includes meta_term_syntax' and 'includes meta_conjunction_syntax'.
2008-08-15 wenzelm 2008-08-15 Args.name_source(_position) for proper position information;
2008-08-13 wenzelm 2008-08-13 tuned document;
2008-06-16 wenzelm 2008-06-16 pervasive RuleInsts;
2008-06-14 wenzelm 2008-06-14 removed unused excluded_middle_tac; proper context for tactics derived from res_inst_tac; tuned setup;
2008-06-10 wenzelm 2008-06-10 eliminated obsolete case_split_thm -- use case_split;
2008-03-29 wenzelm 2008-03-29 purely functional setup of claset/simpset/clasimpset;
2008-03-26 wenzelm 2008-03-26 pass imp_elim, swap to classical prover;
2008-03-15 wenzelm 2008-03-15 added lemmas from simpdata.ML;
2007-10-04 wenzelm 2007-10-04 moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
2007-07-31 wenzelm 2007-07-31 moved classical tools from theory IFOL to FOL;
2007-05-31 wenzelm 2007-05-31 tuned header;
2007-01-20 wenzelm 2007-01-20 tuned ML setup;
2006-11-26 wenzelm 2006-11-26 converted legacy ML scripts;
2006-07-27 wenzelm 2006-07-27 tuned proofs;
2006-01-28 wenzelm 2006-01-28 tuned proofs;
2006-01-06 wenzelm 2006-01-06 simplified EqSubst setup;
2006-01-06 wenzelm 2006-01-06 tuned EqSubst setup;
2005-12-31 wenzelm 2005-12-31 removed obsolete cla_dist_concl;
2005-12-30 wenzelm 2005-12-30 provide cla_dist_concl;
2005-12-23 wenzelm 2005-12-23 removed obsolete induct_atomize_old;
2005-12-22 wenzelm 2005-12-22 updated auxiliary facts for induct method;
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2005-02-01 paulson 2005-02-01 the new subst tactic, by Lucas Dixon
2004-07-08 wenzelm 2004-07-08 removed obsolete dependency;
2003-08-20 paulson 2003-08-20 new case_tac method
2003-07-01 paulson 2003-07-01 moved some lemmas here from ZF
2002-08-30 paulson 2002-08-30 removal of blast.overloaded
2001-12-05 wenzelm 2001-12-05 removed declaration of disjI1, disjI2 (already done in IFOL);
2001-11-28 wenzelm 2001-11-28 tuned;
2001-11-19 wenzelm 2001-11-19 induct method: localize rews for rule;
2001-11-12 wenzelm 2001-11-12 induct_atomize: include atomize_conj (for mutual induction);
2001-11-12 wenzelm 2001-11-12 val local_imp_def = thm "induct_implies_def";
2001-11-09 wenzelm 2001-11-09 theorems case_split = case_split_thm [case_names True False, cases type: o];
2001-10-31 wenzelm 2001-10-31 induct_impliesI;
2001-10-20 wenzelm 2001-10-20 calculational rules moved from FOL to IFOL;
2001-10-14 wenzelm 2001-10-14 moved rulify to ObjectLogic;
2001-10-04 wenzelm 2001-10-04 moved atomize stuff to theory IFOL; added induct/cases setup;
2001-02-11 wenzelm 2001-02-11 tuned trans rules;
2000-11-10 wenzelm 2000-11-10 added atomize_eq;
2000-11-03 wenzelm 2000-11-03 "atomize" for classical tactics;
2000-10-02 wenzelm 2000-10-02 added == transitive rule (bad idea??);
2000-09-07 wenzelm 2000-09-07 setup Rulify.setup;
2000-08-29 wenzelm 2000-08-29 cong setup now part of Simplifier;