| Thu, 02 Oct 2008 14:22:36 +0200 | wenzelm | 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; | file | diff | annotate |
| Mon, 23 Jun 2008 23:45:39 +0200 | wenzelm | Logic.all/mk_equals/mk_implies; | file | diff | annotate |
| Mon, 16 Jun 2008 22:13:52 +0200 | wenzelm | renamed rename_params_tac to rename_tac; | file | diff | annotate |
| Mon, 17 Mar 2008 18:37:00 +0100 | wenzelm | removed duplicate lemmas; | file | diff | annotate |
| Wed, 29 Aug 2007 16:46:08 +0200 | wenzelm | added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy); | file | diff | annotate |