1 files changed, 0 insertions, 122 deletions
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";
-