src/FOL/FOL.thy
2016-05-23 wenzelm 2016-05-23 embedded content may be delimited via cartouches;
2016-01-01 wenzelm 2016-01-01 isabelle update_cartouches -c -t;
2015-10-19 wenzelm 2015-10-19 more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
2015-07-23 wenzelm 2015-07-23 isabelle update_cartouches;
2015-04-09 wenzelm 2015-04-09 clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);
2015-04-06 wenzelm 2015-04-06 tuned;
2015-04-06 wenzelm 2015-04-06 local setup of induction tools, with restricted access to auxiliary consts; proper antiquotations for formerly inaccessible consts;
2015-03-23 wenzelm 2015-03-23 support 'for' fixes in rule_tac etc.;
2015-03-20 wenzelm 2015-03-20 tuned signature;
2015-03-19 wenzelm 2015-03-19 more position information;
2014-11-09 wenzelm 2014-11-09 proper context for match_tac etc.;
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-10-29 wenzelm 2014-10-29 modernized setup;
2014-01-22 wenzelm 2014-01-22 tuned signature;
2013-05-30 wenzelm 2013-05-30 tuned import;
2013-04-27 wenzelm 2013-04-27 uniform Proof.context for hyp_subst_tac;
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2013-04-10 wenzelm 2013-04-10 discontinued obsolete ML antiquotation @{claset};
2012-08-22 wenzelm 2012-08-22 prefer ML_file over old uses;
2012-08-11 wenzelm 2012-08-11 faster compilation of ML with antiquotations: static ML_context is bound once in auxiliary structure Isabelle;
2012-03-15 wenzelm 2012-03-15 declare command keywords via theory header, including strict checking outside Pure;
2011-11-27 wenzelm 2011-11-27 more antiquotations;
2011-11-23 wenzelm 2011-11-23 modernized some old-style infix operations, which were left over from the time of ML proof scripts;
2011-11-20 wenzelm 2011-11-20 tuned;
2011-06-27 wenzelm 2011-06-27 ML antiquotations are managed as theory data, with proper name space and entity markup; clarified Name_Space.check;
2011-05-15 wenzelm 2011-05-15 simplified/unified method_setup/attribute_setup;
2011-05-14 wenzelm 2011-05-14 simplified BLAST_DATA;
2011-05-14 wenzelm 2011-05-14 modernized functor names; tuned;
2011-05-13 wenzelm 2011-05-13 clarified map_simpset versus Simplifier.map_simpset_global;
2011-05-13 wenzelm 2011-05-13 proper Proof.context for classical tactics; reduced claset to snapshot of classical context; discontinued clasimpset;
2011-04-26 wenzelm 2011-04-26 simplified Blast setup;
2011-04-22 wenzelm 2011-04-22 misc tuning and simplification;
2011-04-22 wenzelm 2011-04-22 proper context for Quantifier1 simprocs (avoid bad ProofContext.init_global from abc655166d61); tuned signature;
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;