From 7077e2e8fed4a52af4894954c8446781cb5d40d6 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Tue, 5 Dec 2006 12:49:56 +0000
Subject: Deleted file

---
 isa/Example.ML | 18 ------------------
 1 file changed, 18 deletions(-)
 delete mode 100644 isa/Example.ML

(limited to 'isa/Example.ML')

diff --git a/isa/Example.ML b/isa/Example.ML
deleted file mode 100644
index 57733a48..00000000
--- a/isa/Example.ML
+++ /dev/null
@@ -1,18 +0,0 @@
-(*  -*- isa -*-
-
-    Example proof script for Isabelle Proof General.
-
-    $Id$
-
-    The line at the top of this comment forces 
-    Proof General's classic Isabelle mode
-    (instead of Isar: you can't use both at once).
-*)
-
-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";
-- 
cgit v1.2.3