author | haftmann |
Tue, 09 May 2006 10:11:47 +0200 | |
changeset 19604 | 02f5fbdd5c54 |
parent 19603 | 9801b391c8b3 |
child 19605 | 67e6b4759b37 |
--- 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"