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