src/HOL/Hoare/hoare_tac.ML
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);