diff -r 3e274608f06b -r f9283eb3a4bf src/HOL/Codegenerator_Test/Generate_Pretty.thy --- a/src/HOL/Codegenerator_Test/Generate_Pretty.thy Thu Jun 09 08:32:22 2011 +0200 +++ b/src/HOL/Codegenerator_Test/Generate_Pretty.thy Thu Jun 09 09:07:13 2011 +0200 @@ -10,6 +10,10 @@ lemma [code, code del]: "nat_of_char = nat_of_char" .. lemma [code, code del]: "char_of_nat = char_of_nat" .. +declare Quickcheck_Narrowing.zero_code_int_code[code del] +declare Quickcheck_Narrowing.one_code_int_code[code del] +declare Quickcheck_Narrowing.int_of_code[code del] + subsection {* Check whether generated code compiles *} text {*