diff -r e5508a74b11f -r cb9031a9dccf src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy --- a/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy Wed Aug 25 16:59:53 2010 +0200 +++ b/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy Wed Aug 25 16:59:55 2010 +0200 @@ -182,4 +182,12 @@ 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