src/HOL/ex/Codegenerator.thy
changeset 21319 cf814e36f788
parent 21191 c00161fbf990
child 21404 eb85850d3eb7
     1.1 --- a/src/HOL/ex/Codegenerator.thy	Mon Nov 13 12:10:49 2006 +0100
     1.2 +++ b/src/HOL/ex/Codegenerator.thy	Mon Nov 13 13:51:22 2006 +0100
     1.3 @@ -48,7 +48,7 @@
     1.4    fac :: "int => int" where
     1.5    "fac j = (if j <= 0 then 1 else j * (fac (j - 1)))"
     1.6    by pat_completeness auto
     1.7 -termination by (auto_term "measure nat")
     1.8 +termination by (relation "measure nat") auto
     1.9  
    1.10  declare fac.simps [code]
    1.11