src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy
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)"