From 76440e747b70db646effbd6288c78d4aa04eb0b0 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Thu, 3 Sep 1998 16:24:04 +0000
Subject: Added Isabelle example and skeleton for Coq and Lego.

---
 isa/example.ML | 8 ++++++++
 1 file changed, 8 insertions(+)
 create mode 100644 isa/example.ML

(limited to 'isa/example.ML')

diff --git a/isa/example.ML b/isa/example.ML
new file mode 100644
index 00000000..2357ef55
--- /dev/null
+++ b/isa/example.ML
@@ -0,0 +1,8 @@
+goal HOL.thy "(A & B)-->(B & A)";
+br impI 1;
+br conjI 1;
+be conjE 1;
+ba 1;
+be conjE 1;
+ba 1;
+qed "and_comms";
-- 
cgit v1.2.3