Clean flag settings for profiling. Add AHundredProofs.

1 files changed, 1008 insertions, 0 deletions

diff --git a/etc/isar/AHundredProofs.thy b/etc/isar/AHundredProofs.thy
new file mode 100644
index 00000000..6f59f4e0
--- /dev/null
+++ b/etc/isar/AHundredProofs.thy
@@ -0,0 +1,1008 @@
+theory AHundredProofs imports Main
+begin
+
+ML {* val start = start_timing(); *}
+
+theorem and_comms1: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms2: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms3: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms4: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms5: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms6: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms7: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms8: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms9: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms10: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms11: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms12: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms13: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms14: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms15: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms16: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms17: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms18: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms19: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms20: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms21: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms22: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms23: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms24: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms25: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms26: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms27: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms28: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms29: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms30: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms31: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms32: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms33: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms34: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms35: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms36: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms37: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms38: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms39: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms40: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms41: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms42: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms43: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms44: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms45: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms46: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms47: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms48: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms49: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms50: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms51: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms52: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms53: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms54: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms55: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms56: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms57: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms58: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms59: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms60: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms61: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms62: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms63: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms64: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms65: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms66: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms67: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms68: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms69: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms70: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms71: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms72: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms73: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms74: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms75: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms76: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms77: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms78: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms79: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms80: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms81: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms82: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms83: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms84: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms85: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms86: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms87: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms88: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms89: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms90: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms91: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms92: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms93: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms94: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms95: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms96: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms97: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms98: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms99: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+theorem and_comms100: "A & B --> B & A"
+proof
+  assume "A & B"
+  then show "B & A"
+  proof
+    assume B and A
+    then show ?thesis ..
+ qed
+qed
+
+ML {* Output.warning (#message (end_timing start)); *}
+
+end