src/HOL/Predicate_Compile_Examples/Examples.thy
changeset 42094 e6867e9c6d10
parent 41413 64cd30d6b0b8
child 42187 b4f4ed5b8586
     1.1 --- a/src/HOL/Predicate_Compile_Examples/Examples.thy	Thu Mar 24 10:39:47 2011 +0100
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Examples.thy	Thu Mar 24 15:29:31 2011 +0100
     1.3 @@ -291,6 +291,12 @@
     1.4  
     1.5  thm big_step.equation
     1.6  
     1.7 +definition list :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a list" where
     1.8 +  "list s n = map s [0 ..< n]"
     1.9 +
    1.10 +values [expected "{[42, (43 :: nat)]}"] "{list s 2|s. (SKIP, nth [42, 43]) \<Rightarrow> s}"
    1.11 +
    1.12 +
    1.13  subsection {* CCS *}
    1.14  
    1.15  text{* This example formalizes finite CCS processes without communication or