1.1 --- a/src/HOL/Statespace/StateSpaceEx.thy	Mon Nov 07 17:54:38 2011 +0100
     1.2 +++ b/src/HOL/Statespace/StateSpaceEx.thy	Mon Nov 07 21:32:59 2011 +0100
     1.3 @@ -476,4 +476,8 @@
     1.4  A987::nat A988::nat A989::nat A990::nat A991::nat A992::nat A993::nat
     1.5  A994::nat A995::nat A996::nat A997::nat A998::nat A999::nat A1000::nat
     1.6  
     1.7 +lemma (in benchmark100) test: "s<A1 := a>\<cdot>A100 = s\<cdot>A100" by simp
     1.8 +lemma (in benchmark500) test: "s<A1 := a>\<cdot>A100 = s\<cdot>A100" by simp
     1.9 +lemma (in benchmark1000) test: "s<A1 := a>\<cdot>A100 = s\<cdot>A100" by simp
    1.10 +
    1.11  end