equal
deleted
inserted
replaced
329 qed |
329 qed |
330 qed |
330 qed |
331 |
331 |
332 subsection \<open>Preprocessor Inlining\<close> |
332 subsection \<open>Preprocessor Inlining\<close> |
333 |
333 |
334 definition "equals == (op =)" |
334 definition "equals == (=)" |
335 |
335 |
336 inductive zerozero' :: "nat * nat => bool" where |
336 inductive zerozero' :: "nat * nat => bool" where |
337 "equals (x, y) (0, 0) ==> zerozero' (x, y)" |
337 "equals (x, y) (0, 0) ==> zerozero' (x, y)" |
338 |
338 |
339 code_pred (expected_modes: i => bool) zerozero' . |
339 code_pred (expected_modes: i => bool) zerozero' . |