# HG changeset patch
# User bulwahn
# Date 1257491518 -3600
# Node ID 1272cfc7b910416f3627daeb61a07e92e9c9520a
# Parent  27cca5416a88a391e9eae5cd990c712e80112237
added further example of the values command

diff -r 27cca5416a88 -r 1272cfc7b910 src/HOL/ex/Predicate_Compile_ex.thy
--- a/src/HOL/ex/Predicate_Compile_ex.thy	Fri Nov 06 08:11:58 2009 +0100
+++ b/src/HOL/ex/Predicate_Compile_ex.thy	Fri Nov 06 08:11:58 2009 +0100
@@ -257,14 +257,14 @@
     "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]}"
@@ -541,10 +541,13 @@
 
 code_pred steps .
 
+values 3 
+ "{as . steps (par (or (pre 0 nil) (pre 1 nil)) (pre 2 nil)) as (par nil nil)}"
+
 values 5
  "{as . steps (par (or (pre 0 nil) (pre 1 nil)) (pre 2 nil)) as (par nil nil)}"
 
-(* FIXME
+(* FIXME:
 values 3 "{(a,q). step (par nil nil) a q}"
 *)