# HG changeset patch
# User bulwahn
# Date 1272465951 -7200
# Node ID db2953f5887af99c6aca9a407da013324006468e
# Parent  d716eb002b9fb0cbf02a6df02b962b67953916b5
added an example with a free function variable to the Predicate Compile examples

diff -r d716eb002b9f -r db2953f5887a src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy	Wed Apr 28 16:45:50 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy	Wed Apr 28 16:45:51 2010 +0200
@@ -686,6 +686,13 @@
 (*values [depth_limit = 4] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *)
 (*values [depth_limit = 20] "{x. not_reachable_in_example_graph' 0 4}"*) (* fails with undefined *)
 
+subsection {* Free function variable *}
+
+inductive FF :: "nat => nat => bool"
+where
+  "f x = y ==> FF x y"
+
+code_pred FF .
 
 subsection {* IMP *}