changeset 26480 | 544cef16045b |
parent 25475 | d5a382ccb5cc |
child 29667 | 53103fc8ffa3 |
--- a/src/HOL/ex/Lagrange.thy Sat Mar 29 19:13:58 2008 +0100 +++ b/src/HOL/ex/Lagrange.thy Sat Mar 29 19:14:00 2008 +0100 @@ -25,7 +25,7 @@ (* These two simprocs are even less efficient than ordered rewriting and kill the second example: *) -ML_setup {* +ML {* Delsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv] *}