1 files changed, 0 insertions, 20 deletions
diff --git a/isa/Example-Xsym.ML b/isa/Example-Xsym.ML
deleted file mode 100644
index ed97c291..00000000
--- a/isa/Example-Xsym.ML
+++ /dev/null
@@ -1,20 +0,0 @@
-(*
-    Example proof script for Isabelle Proof General.
-
-    $Id$
-
-    Just a version of Example.ML using XSymbol.
-
-    Also subscripts/superscripts:  A\<^sup>1 \\<or> A\<^sub>2
-    [NB: these can't be used in identifiers or otherwise
-     parsed by Isabelle unless declared as part of a theory's 
-     concrete syntax, see docs or examples in HOL/IMP.]
-*)    
-
-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";