src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy

 where
   "y \<noteq> A \<Longrightarrow> z \<noteq> B \<Longrightarrow> notAB (y, z)"
 
 values 5 "{y. notAB y}"
 
+section {* Example prolog conform variable names *}
+
+inductive equals :: "abc => abc => bool"
+where
+  "equals y' y'"
+ML {* set Code_Prolog.trace *}
+values 1 "{(y, z). equals y z}"
+
 end