src/HOL/Codegenerator_Test/Generate_Pretty.thy
changeset 47108 2a1953f0d20d
parent 43317 f9283eb3a4bf
child 50629 264ece81df93
--- a/src/HOL/Codegenerator_Test/Generate_Pretty.thy	Sat Mar 24 16:27:04 2012 +0100
+++ b/src/HOL/Codegenerator_Test/Generate_Pretty.thy	Sun Mar 25 20:15:39 2012 +0200
@@ -10,9 +10,8 @@
 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]
+declare Quickcheck_Narrowing.one_code_int_code [code del]
+declare Quickcheck_Narrowing.int_of_code [code del]
 
 subsection {* Check whether generated code compiles *}