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.

---
 coq/example.v  | 2 ++
 isa/example.ML | 8 ++++++++
 lego/example.l | 2 ++
 3 files changed, 12 insertions(+)
 create mode 100644 coq/example.v
 create mode 100644 isa/example.ML
 create mode 100644 lego/example.l

diff --git a/coq/example.v b/coq/example.v
new file mode 100644
index 00000000..c9c88d9e
--- /dev/null
+++ b/coq/example.v
@@ -0,0 +1,2 @@
+
+INSERT HANDY COQ EXAMPLE HERE!
\ No newline at end of file
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";
diff --git a/lego/example.l b/lego/example.l
new file mode 100644
index 00000000..c82e7b2c
--- /dev/null
+++ b/lego/example.l
@@ -0,0 +1,2 @@
+
+INSERT HANDY LEGO EXAMPLE HERE!
\ No newline at end of file
-- 
cgit v1.2.3