changeset 30510 | 4120fc59dd85 |
parent 26187 | 3e099fc47afd |
child 30549 | d2d7874648bd |
--- a/src/HOL/ex/Binary.thy Fri Mar 13 19:53:09 2009 +0100 +++ b/src/HOL/ex/Binary.thy Fri Mar 13 19:58:26 2009 +0100 @@ -174,7 +174,7 @@ simproc_setup binary_nat_mod ("m mod (n::nat)") = {* K (divmod_proc @{thm binary_divmod(2)}) *} method_setup binary_simp = {* - Method.no_args (Method.SIMPLE_METHOD' + Method.no_args (SIMPLE_METHOD' (full_simp_tac (HOL_basic_ss addsimps @{thms binary_simps}