| changeset 47432 | e1576d13e933 |
| parent 44890 | 22f665a2e91c |
| child 51717 | 9e7d1c139569 |
--- a/src/HOL/Auth/Smartcard/ShoupRubin.thy Thu Apr 12 11:34:50 2012 +0200 +++ b/src/HOL/Auth/Smartcard/ShoupRubin.thy Thu Apr 12 18:39:19 2012 +0200 @@ -762,7 +762,7 @@ method_setup prepare = {* Scan.succeed (K (SIMPLE_METHOD ShoupRubin.prepare_tac)) *} - "to launch a few simple facts that'll help the simplifier" + "to launch a few simple facts that will help the simplifier" method_setup parts_prepare = {* Scan.succeed (fn ctxt => SIMPLE_METHOD (ShoupRubin.parts_prepare_tac ctxt)) *}