properly merged
authorhaftmann
Mon Aug 10 13:34:50 2009 +0200 (2009-08-10)
changeset 32355806d2df4d79d
parent 32354 bb40e900e1f3
child 32356 e11cd88e6ade
properly merged
src/HOL/ex/Predicate_Compile_ex.thy
     1.1 --- a/src/HOL/ex/Predicate_Compile_ex.thy	Mon Aug 10 12:25:30 2009 +0200
     1.2 +++ b/src/HOL/ex/Predicate_Compile_ex.thy	Mon Aug 10 13:34:50 2009 +0200
     1.3 @@ -38,7 +38,6 @@
     1.4  thm rev.equation
     1.5  
     1.6  values "{xs. rev [0, 1, 2, 3::nat] xs}"
     1.7 -values "Collect (rev [0, 1, 2, 3::nat])"
     1.8  
     1.9  inductive partition :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
    1.10    for f where
    1.11 @@ -56,10 +55,8 @@
    1.12  
    1.13  code_pred is_even .
    1.14  
    1.15 -(* TODO: requires to handle abstractions in parameter positions correctly *)
    1.16  values 10 "{(ys, zs). partition is_even
    1.17    [0, Suc 0, 2, 3, 4, 5, 6, 7] ys zs}"
    1.18 -
    1.19  values 10 "{zs. partition is_even zs [0, 2] [3, 5]}"
    1.20  values 10 "{zs. partition is_even zs [0, 7] [3, 5]}"
    1.21  
    1.22 @@ -89,16 +86,13 @@
    1.23  code_pred succ .
    1.24  
    1.25  thm succ.equation
    1.26 -<<<<<<< local
    1.27  
    1.28  values 10 "{(m, n). succ n m}"
    1.29  values "{m. succ 0 m}"
    1.30  values "{m. succ m 0}"
    1.31  
    1.32 -(* FIXME: why does this not terminate? *)
    1.33 -=======
    1.34  (* FIXME: why does this not terminate? -- value chooses mode [] --> [1] and then starts enumerating all successors *)
    1.35 ->>>>>>> other
    1.36 +
    1.37  (*
    1.38  values 20 "{n. tranclp succ 10 n}"
    1.39  values "{n. tranclp succ n 10}"