equal
deleted
inserted
replaced
8 begin |
8 begin |
9 |
9 |
10 lemma [code, code del]: "nat_of_char = nat_of_char" .. |
10 lemma [code, code del]: "nat_of_char = nat_of_char" .. |
11 lemma [code, code del]: "char_of_nat = char_of_nat" .. |
11 lemma [code, code del]: "char_of_nat = char_of_nat" .. |
12 |
12 |
13 declare Quickcheck_Narrowing.one_code_int_code [code del] |
|
14 declare Quickcheck_Narrowing.int_of_code [code del] |
|
15 |
|
16 subsection {* Check whether generated code compiles *} |
13 subsection {* Check whether generated code compiles *} |
17 |
14 |
18 text {* |
15 text {* |
19 If any of the checks fails, inspect the code generated |
16 If any of the checks fails, inspect the code generated |
20 by a corresponding @{text export_code} command. |
17 by a corresponding @{text export_code} command. |