changeset 67399 | eab6ce8368fa |
parent 67226 | ec32cdaab97b |
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy Wed Jan 10 15:21:49 2018 +0100 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy Wed Jan 10 15:25:09 2018 +0100 @@ -331,7 +331,7 @@ subsection \<open>Preprocessor Inlining\<close> -definition "equals == (op =)" +definition "equals == (=)" inductive zerozero' :: "nat * nat => bool" where "equals (x, y) (0, 0) ==> zerozero' (x, y)"