aboutsummaryrefslogtreecommitdiff
path: root/isa/example.ML
diff options
context:
space:
mode:
Diffstat (limited to 'isa/example.ML')
-rw-r--r--isa/example.ML14
1 files changed, 0 insertions, 14 deletions
diff --git a/isa/example.ML b/isa/example.ML
deleted file mode 100644
index 41ea20be..00000000
--- a/isa/example.ML
+++ /dev/null
@@ -1,14 +0,0 @@
-(*
- Example proof script for Isabelle Proof General.
-
- $Id$
-*)
-
-Goal "(A & B)-->(B & A)";
-br impI 1;
-br conjI 1;
-be conjE 1;
-ba 1;
-be conjE 1;
-ba 1;
-qed "and_comms";