# 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\A100 = s\A100" by simp +lemma (in benchmark500) test: "s\A100 = s\A100" by simp +lemma (in benchmark1000) test: "s\A100 = s\A100" by simp + end