From bd7aa7923a25d16207842f9f3d6b773c2fc6fa58 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Thu, 28 Sep 2000 15:01:50 +0000
Subject: Renamed file
---
html/links.html | 71 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++
1 file changed, 71 insertions(+)
create mode 100644 html/links.html
(limited to 'html/links.html')
diff --git a/html/links.html b/html/links.html
new file mode 100644
index 00000000..32ac9782
--- /dev/null
+++ b/html/links.html
@@ -0,0 +1,71 @@
+Related projects
+
+Here are some links to related things.
+If you have any suggestions
+for links to include here, please
+.
+
+
+
+- Isamode
+ is an XEmacs front-end for Isabelle. It has a different
+ feature collection compared with Proof General:
+ script management is not supported, but there are extensive
+ menus and shortcuts provided for common Isabelle
+ commands.
+
+
+
+- CtCoq
+ is an interface for the Coq theorem prover, developed
+ at INRIA, Sophia Antipolis, as part of
+ Projet CROAP.
+ Like Proof General, CtCoq is based on a general approach for
+ building user-interfaces for theorem provers, although no other
+ current theorem provers are supported. Unlike Proof General, CtCoq
+ is based on a graphical environment with structure editing,
+ created with the Centaur
+ system.
+
+
+
+-
+ OMEGA is
+ a collection of web-based distributed tools for supporting
+ theorem proving.
+
+
+
+-
+ Prosper is a project
+ to develop an extensible, open proof tool architecture for
+ incorporating formal verification into industrial CAD/CASE tool
+ flows and design methodologies. The tools include novel
+ user-friendly interfaces.
+
+
+
+-
+ As a possible foundation for generic proof environments,
+ OpenMath
+ is a standard representation form for mathematical objects, which
+ links in with the MathML
+ markup language.
+
+
+
+
+
--
cgit v1.2.3