From 45b1cff194b0dbd38d39cf5175d100b88a55792a Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Fri, 16 Apr 2004 10:00:44 +0000 Subject: Updated. --- README | 9 ++++++++- etc/announce | 1 + 2 files changed, 9 insertions(+), 1 deletion(-) diff --git a/README b/README index a28ec3aa..eaf4f852 100644 --- a/README +++ b/README @@ -54,6 +54,13 @@ in the subdirectories: generic/ Generic basis for Proof General +A small number of example proofs are included in each prover +subdirectory. The "root2" example proofs of the irrationality +of the square root of 2 were proofs written as a response +to a challenge of Freek Wiedijk in his comparison of different +theorem provers, see http://www.cs.kun.nl/~freek/comparison/. +Those proof scripts are copyright by their named authors. + Check BUGS files for problems and issues, in this directory, and for specific issues, in each prover subdirectory. Please report bugs not mentioned in any of these files to da+pg-bugs@inf.ed.ac.uk @@ -62,4 +69,4 @@ For the latest news and downloads, visit Proof General on the web at: http://proofgeneral.inf.ed.ac.uk David Aspinall -March 2004. +April 2004. diff --git a/etc/announce b/etc/announce index c614932e..811b48c7 100644 --- a/etc/announce +++ b/etc/announce @@ -32,6 +32,7 @@ Summary of interesting changes since 3.4: . For Coq: a new "holes" system, for editing structured expressions . For Isabelle: browsing/highlighting theorem dependencies . New instances of PG: Casl Consistency Checker, Shell Script +. Additional sample proofs (some from http://www.cs.kun.nl/~freek/comparison/) . Many other minor improvements and editing features . Many changes for compatibility with latest Emacsen (esp. GNU) and provers -- cgit v1.2.3