src/HOL/Predicate_Compile_Examples/Examples.thy
changeset 51144 0ede9e2266a8
parent 45970 b6d0cff57d96
child 52666 391913d17d15
     1.1 --- a/src/HOL/Predicate_Compile_Examples/Examples.thy	Fri Feb 15 08:31:31 2013 +0100
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Examples.thy	Fri Feb 15 08:31:31 2013 +0100
     1.3 @@ -309,7 +309,14 @@
     1.4  definition list :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a list" where
     1.5    "list s n = map s [0 ..< n]"
     1.6  
     1.7 -values [expected "{[42, (43 :: nat)]}"] "{list s 2|s. (SKIP, nth [42, 43]) \<Rightarrow> s}"
     1.8 +values [expected "{[Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
     1.9 +     (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
    1.10 +     (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)
    1.11 +     )))))))))))))))))))))))))))))))))))))))),
    1.12 +   Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc   (Suc (Suc (Suc (Suc
    1.13 +     (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
    1.14 +     (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)
    1.15 +     )))))))))))))))))))))))))))))))))))))))))]}"] "{list s 2|s. (SKIP, nth [42, 43]) \<Rightarrow> s}"
    1.16  
    1.17  
    1.18  subsection {* CCS *}