1 files changed, 0 insertions, 15 deletions
diff --git a/isa/Example2.ML b/isa/Example2.ML
deleted file mode 100644
index ab2fef03..00000000
--- a/isa/Example2.ML
+++ /dev/null
@@ -1,15 +0,0 @@
-(*
-    Example proof script for Isabelle Proof General.
-
-    $Id$
-
-    Same as Example.ML, except using X-Symbol input tokens.
-*)
-
-Goal "A \\<and> B \\<longrightarrow> B \\<and> A";
-  by (rtac impI 1);
-  by (etac conjE 1);
-  by (rtac conjI 1);
-  by (assume_tac 1);
-  by (assume_tac 1);
-qed "and_comms";