src/HOL/IntDiv.thy
changeset 26480 544cef16045b
parent 26101 a657683e902a
child 26507 6da615cef733
     1.1 --- a/src/HOL/IntDiv.thy	Sat Mar 29 19:13:58 2008 +0100
     1.2 +++ b/src/HOL/IntDiv.thy	Sat Mar 29 19:14:00 2008 +0100
     1.3 @@ -257,7 +257,7 @@
     1.4  
     1.5  text {* Tool setup *}
     1.6  
     1.7 -ML_setup {*
     1.8 +ML {*
     1.9  local 
    1.10  
    1.11  structure CancelDivMod = CancelDivModFun(