From 2a5709c354e09b06556f3f1e19bf2d9a5ad91564 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Fri, 2 Apr 2004 16:58:54 +0000 Subject: Updated. --- hol98/README | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'hol98') diff --git a/hol98/README b/hol98/README index e6c3b4b3..69372fc9 100644 --- a/hol98/README +++ b/hol98/README @@ -37,7 +37,7 @@ Emacs interface by Koichi Takahashi and Masima Hagiya addressed this, and to some extent so perhaps does the Emacs interface supplied with HOL. Perhaps one of these could be embedded/reimplemented inside Proof General. Implemented in a generic way, managing batch vs -interactive proofs would also be useful for Isabelle. +interactive proofs might also be useful for Isabelle. Another problem is that HOL scripts sometimes use SML structures, which can cause confusion because Proof General does not really parse -- cgit v1.2.3