# HG changeset patch
# User haftmann
# Date 1249904090 -7200
# Node ID 806d2df4d79d66cf874b80f641117b30ac9ab2f4
# Parent  bb40e900e1f3925fb0b067cfa03be272fb95468f
properly merged

diff -r bb40e900e1f3 -r 806d2df4d79d src/HOL/ex/Predicate_Compile_ex.thy
--- a/src/HOL/ex/Predicate_Compile_ex.thy	Mon Aug 10 12:25:30 2009 +0200
+++ b/src/HOL/ex/Predicate_Compile_ex.thy	Mon Aug 10 13:34:50 2009 +0200
@@ -38,7 +38,6 @@
 thm rev.equation
 
 values "{xs. rev [0, 1, 2, 3::nat] xs}"
-values "Collect (rev [0, 1, 2, 3::nat])"
 
 inductive partition :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
   for f where
@@ -56,10 +55,8 @@
 
 code_pred is_even .
 
-(* TODO: requires to handle abstractions in parameter positions correctly *)
 values 10 "{(ys, zs). partition is_even
   [0, Suc 0, 2, 3, 4, 5, 6, 7] ys zs}"
-
 values 10 "{zs. partition is_even zs [0, 2] [3, 5]}"
 values 10 "{zs. partition is_even zs [0, 7] [3, 5]}"
 
@@ -89,16 +86,13 @@
 code_pred succ .
 
 thm succ.equation
-<<<<<<< local
 
 values 10 "{(m, n). succ n m}"
 values "{m. succ 0 m}"
 values "{m. succ m 0}"
 
-(* FIXME: why does this not terminate? *)
-=======
 (* FIXME: why does this not terminate? -- value chooses mode [] --> [1] and then starts enumerating all successors *)
->>>>>>> other
+
 (*
 values 20 "{n. tranclp succ 10 n}"
 values "{n. tranclp succ n 10}"