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