changeset 19604 | 02f5fbdd5c54 |
parent 19281 | b411f25fff25 |
child 19789 | c08c9f9ea9a5 |
--- a/src/HOL/ex/Codegenerator.thy Tue May 09 10:11:30 2006 +0200 +++ b/src/HOL/ex/Codegenerator.thy Tue May 09 10:11:47 2006 +0200 @@ -55,7 +55,7 @@ "fac j = (if j <= 0 then 1 else j * (fac (j - 1)))" code_generate - "0::int" "1::int" k + "0::int" k "op + :: int \<Rightarrow> int \<Rightarrow> int" "op - :: int \<Rightarrow> int \<Rightarrow> int" "op * :: int \<Rightarrow> int \<Rightarrow> int"