changeset 21588 | cd0dc678a205 |
parent 21404 | eb85850d3eb7 |
child 22741 | 4bd02e03305c |
--- a/src/HOL/Isar_examples/Hoare.thy Wed Nov 29 15:44:46 2006 +0100 +++ b/src/HOL/Isar_examples/Hoare.thy Wed Nov 29 15:44:51 2006 +0100 @@ -447,7 +447,7 @@ method_setup hoare = {* Method.no_args - (Method.SIMPLE_METHOD' HEADGOAL + (Method.SIMPLE_METHOD' (hoare_tac (simp_tac (HOL_basic_ss addsimps [thm "Record.K_record_apply"] )))) *} "verification condition generator for Hoare logic"