--- a/src/HOL/ex/Predicate_Compile_ex.thy Thu Nov 05 14:47:27 2009 +0100
+++ b/src/HOL/ex/Predicate_Compile_ex.thy Fri Nov 06 08:11:58 2009 +0100
@@ -247,13 +247,15 @@
"append [] xs xs"
| "append xs ys zs \<Longrightarrow> append (x # xs) ys (x # zs)"
-code_pred (mode: [1, 2], [3], [2, 3], [1, 3], [1, 2, 3]) append .
+(*code_pred (mode: [1, 2], [3], [2, 3], [1, 3], [1, 2, 3]) append .*)
code_pred [depth_limited] append .
-code_pred [random] append .
+(*code_pred [random] append .*)
+code_pred [annotated] append .
-thm append.equation
+(*thm append.equation
thm append.depth_limited_equation
-thm append.random_equation
+thm append.random_equation*)
+thm append.annotated_equation
values "{(ys, xs). append xs ys [0, Suc 0, 2]}"
values "{zs. append [0, Suc 0, 2] [17, 8] zs}"