# HG changeset patch
# User wenzelm
# Date 1320697979 -3600
# Node ID 94b5016c05c3c5247dc2abc8284b4317b55769e2
# Parent  13ab80eafd71ec4d6421a97bad77d8926d24c2af
more benchmarks;

diff -r 13ab80eafd71 -r 94b5016c05c3 src/HOL/Statespace/StateSpaceEx.thy
--- 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