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