src/HOL/Hoare/hoare_tac.ML
2015-10-13 haftmann 2015-10-13 prod_case as canonical name for product type eliminator
2015-09-06 haftmann 2015-09-06 prefer "uncurry" as canonical name for case distinction on products in combinatorial view
2015-07-18 wenzelm 2015-07-18 prefer tactics with explicit context;
2014-02-21 wenzelm 2014-02-21 tuned whitespace; tuned names;
2014-02-21 wenzelm 2014-02-21 proper ML structure with signature;
2014-02-21 wenzelm 2014-02-21 reduced ML warnings;
2014-02-12 blanchet 2014-02-12 renamed '{prod,sum,bool,unit}_case' to 'case_...'
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2011-08-17 wenzelm 2011-08-17 modernized signature of Term.absfree/absdummy; eliminated obsolete Term.list_abs_free;
2011-05-13 wenzelm 2011-05-13 proper Proof.context for classical tactics; reduced claset to snapshot of classical context; discontinued clasimpset;
2011-01-07 wenzelm 2011-01-07 do not open ML structures;
2010-07-27 haftmann 2010-07-27 delete structure Basic_Record; avoid `record` in names in structure Record
2010-07-01 haftmann 2010-07-01 qualified constants Set.member and Set.Collect
2010-06-28 haftmann 2010-06-28 merged constants "split" and "prod_case"
2010-06-10 haftmann 2010-06-10 tuned quotes, antiquotations and whitespace
2010-05-26 haftmann 2010-05-26 dropped legacy theorem bindings
2010-05-26 haftmann 2010-05-26 normalized references to constant "split"
2010-02-10 haftmann 2010-02-10 moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
2010-01-28 haftmann 2010-01-28 new theory Algebras.thy for generic algebraic structures
2009-07-23 wenzelm 2009-07-23 renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
2008-10-02 wenzelm 2008-10-02 major cleanup of hoare_tac.ML: just one copy for Hoare.thy and HoareAbort.thy (only 1 line different), refrain from inspecting the main goal, proper context;
2008-06-23 wenzelm 2008-06-23 Logic.all/mk_equals/mk_implies;
2008-06-16 wenzelm 2008-06-16 renamed rename_params_tac to rename_tac;
2008-03-17 wenzelm 2008-03-17 removed duplicate lemmas;
2007-08-29 wenzelm 2007-08-29 added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);