aboutsummaryrefslogtreecommitdiff
path: root/isa/Example.ML
diff options
context:
space:
mode:
authorDavid Aspinall2006-12-05 12:49:56 +0000
committerDavid Aspinall2006-12-05 12:49:56 +0000
commit7077e2e8fed4a52af4894954c8446781cb5d40d6 (patch)
tree023224bae2e0e278d99e94bba2f0d3fe98984495 /isa/Example.ML
parent1ea338cca92204c9a98a373adb80ab60c3a10107 (diff)
Deleted file
Diffstat (limited to 'isa/Example.ML')
-rw-r--r--isa/Example.ML18
1 files changed, 0 insertions, 18 deletions
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";