# HG changeset patch
# User wenzelm
# Date 1325592363 -3600
# Node ID 65bde43e829c3e0ca5c8a168f4fba627debada75
# Parent  629aaafd3af6ebaf32ad041016f840f0a3502a63
more benchmarks;
tuned;

diff -r 629aaafd3af6 -r 65bde43e829c src/HOL/Record_Benchmark/Record_Benchmark.thy
--- a/src/HOL/Record_Benchmark/Record_Benchmark.thy	Mon Jan 02 20:25:21 2012 +0100
+++ b/src/HOL/Record_Benchmark/Record_Benchmark.thy	Tue Jan 03 13:06:03 2012 +0100
@@ -312,6 +312,39 @@
 A298::nat
 A299::nat
 
+record many_B = many_A +
+B000::nat
+B001::nat
+B002::nat
+B003::nat
+B004::nat
+B005::nat
+B006::nat
+B007::nat
+B008::nat
+B009::nat
+B010::nat
+B011::nat
+B012::nat
+B013::nat
+B014::nat
+B015::nat
+B016::nat
+B017::nat
+B018::nat
+B019::nat
+B020::nat
+B021::nat
+B022::nat
+B023::nat
+B024::nat
+B025::nat
+B026::nat
+B027::nat
+B028::nat
+B029::nat
+B030::nat
+
 lemma "A155 (r\<lparr>A255:=x\<rparr>) = A155 r"
   by simp
 
@@ -366,20 +399,16 @@
   done
 
 
-lemma True
-proof -
-  {
-    fix P r
-    assume pre: "P (A155 r)"
-    have "\<exists>x. P x"
-      using pre
-      apply -
-      apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
-      apply auto 
-      done
-  }
-  show ?thesis ..
-qed
+notepad
+begin
+  fix P r
+  assume "P (A155 r)"
+  then have "\<exists>x. P x"
+    apply -
+    apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
+    apply auto 
+    done
+end
 
 
 lemma "\<exists>r. A155 r = x"