From a6df07141665078a6f090a4dd20571fb9c0a68fd Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Mon, 3 Sep 2001 21:46:29 +0000
Subject: Accidental commit; revert to original.

---
 isa/Example.ML | 122 ---------------------------------------------------------
 1 file changed, 122 deletions(-)

(limited to 'isa/Example.ML')

diff --git a/isa/Example.ML b/isa/Example.ML
index b1ad1ee2..4ef88eaa 100644
--- a/isa/Example.ML
+++ b/isa/Example.ML
@@ -13,125 +13,3 @@ Goal "A & B --> B & A";
 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