From b7209db785ccd5e68ecc144f628cf7593a215ede Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Mon, 3 Sep 2001 12:11:59 +0000
Subject: Updating branch

---
 isa/Example.ML | 123 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 123 insertions(+)

(limited to 'isa/Example.ML')

diff --git a/isa/Example.ML b/isa/Example.ML
index c607390f..b1ad1ee2 100644
--- a/isa/Example.ML
+++ b/isa/Example.ML
@@ -12,3 +12,126 @@ Goal "A & B --> B & A";
   by (assume_tac 1);
 qed "and_comms";
 
+
+Goal "A & B --> B & A";
+  by (rtac impI 1);
+  by (etac conjE 1);
+  by (rtac conjI 1);
+  by (assume_tac 1);
+  by (assume_tac 1);
+qed "and_comms2";
+
+
+Goal "A & B --> B & A";
+  by (rtac impI 1);
+  by (etac conjE 1);
+  by (rtac conjI 1);
+  by (assume_tac 1);
+  by (assume_tac 1);
+qed "and_comms3";
+
+
+Goal "A & B --> B & A";
+  by (rtac impI 1);
+  by (etac conjE 1);
+  by (rtac conjI 1);
+  by (assume_tac 1);
+  by (assume_tac 1);
+qed "and_comms8";
+
+
+Goal "A & B --> B & A";
+  by (rtac impI 1);
+  by (etac conjE 1);
+  by (rtac conjI 1);
+  by (assume_tac 1);
+  by (assume_tac 1);
+qed "and_comms";
+
+
+Goal "A & B --> B & A";
+  by (rtac impI 
+  by (etac conjE 1);
+  by (rtac conjI 1);
+  by (assume_tac 1);
+  by (assume_tac 1);
+qed "and_comms3";
+
+Goal "A & B --> B & A";
+  by (rtac impI 1);
+  by (etac conjE 1);
+  by (rtac conjI 1);
+  by (assume_tac 1);
+  by (assume_tac 1);
+qed "and_comms";
+
+
+Goal "A & B --> B & A";
+  by (rtac impI 1);
+  by (etac conjE 1);
+  by (rtac conjI 1);
+  by (assume_tac 1);
+  by (assume_tac 1);
+qed "and_comms";
+
+
+Goal "A & B --> B & A";
+  by (rtac impI 1);
+  by (etac conjE 1);
+  by (rtac conjI 1);
+  by (assume_tac 1);
+  by (assume_tac 1);
+qed "and_comms3";
+
+Goal "A & B --> B & A";
+  by (rtac impI 1);
+  by (etac conjE 1);
+  by (rtac conjI 1);
+  by (assume_tac 1);
+  by (assume_tac 1);
+qed "and_comms";
+
+
+Goal "A & B --> B & A";
+  by (rtac impI 1);
+  by (etac conjE 1);
+  by (rtac conjI 1);
+  by (assume_tac 1);
+  by (assume_tac 1);
+qed "and_comms";
+
+
+Goal "A & B --> B & A";
+  by (rtac impI 1);
+  by (etac conjE 1);
+  by (rtac conjI 1);
+  by (assume_tac 1);
+  by (assume_tac 1);
+qed "and_comms3";
+
+Goal "A & B --> B & A";
+  by (rtac impI 1);
+  by (etac conjE 1);
+  by (rtac conjI 1);
+  by (assume_tac 1);
+  by (assume_tac 1);
+qed "and_comms";
+
+
+Goal "A & B --> B & A";
+  by (rtac impI 1);
+  by (etac conjE 1);
+  by (rtac conjI 1);
+  by (assume_tac 1);
+  by (assume_tac 1);
+qed "and_comms";
+
+
+Goal "A & B --> B & A";
+  by (rtac impI 1);
+  by (etac conjE 1);
+  by (rtac conjI 1);
+  by (assume_tac 1);
+  by (assume_tac 1);
+qed "and_comms3";
+
-- 
cgit v1.2.3