# HG changeset patch
# User wenzelm
# Date 982078278 -3600
# Node ID ce1cefc6c14cb8f45f374bb225aae365259a360b
# Parent 43791f99d71e770c535b9f1fb037fcfabbafc985
tuned;
diff -r 43791f99d71e -r ce1cefc6c14c ANNOUNCE
--- a/ANNOUNCE Tue Feb 13 16:05:56 2001 +0100
+++ b/ANNOUNCE Tue Feb 13 16:31:18 2001 +0100
@@ -12,22 +12,22 @@
* Poly/ML 4.0 used by default
More robust, less disk space required.
- * Pure/Simplifier (Stefan Berghofer)
+ * Simplifier (Stefan Berghofer)
Proper implementation as a derived rule, outside the kernel!
+ * Improved document preparation (Markus Wenzel)
+ Near math-mode, sub/super scripts, more symbols etc.
+
* Isabelle/Isar (Markus Wenzel)
Numerous usability improvements, e.g. support for initial
schematic goals, failure prediction of subgoal statements,
handling of non-atomic statements in induction.
- * Improved document preparation (Markus Wenzel)
- Near math-mode, sub/super scripts, more symbols etc.
-
* HOL/Library (Gertrud Bauer, Tobias Nipkow, Lawrence C Paulson,
Thomas M Rasmussen, Markus Wenzel)
A collection of generic theories to be used together with main HOL.
- * HOL/Real and HOL/Hyperreal (Jacques Fleuriot and Lawrence C Paulson)
+ * HOL/Real and HOL/Hyperreal (Jacques Fleuriot, Lawrence C Paulson)
General cleanup, more on nonstandard real analysis.
* HOL/Unix (Markus Wenzel)
diff -r 43791f99d71e -r ce1cefc6c14c Admin/page/dist-content/docs.content
--- a/Admin/page/dist-content/docs.content Tue Feb 13 16:05:56 2001 +0100
+++ b/Admin/page/dist-content/docs.content Tue Feb 13 16:31:18 2001 +0100
@@ -13,10 +13,10 @@
information about the present release and additional installation
instructions.
diff -r 43791f99d71e -r ce1cefc6c14c Admin/page/dist-content/index.content
--- a/Admin/page/dist-content/index.content Tue Feb 13 16:05:56 2001 +0100
+++ b/Admin/page/dist-content/index.content Tue Feb 13 16:31:18 2001 +0100
@@ -11,18 +11,18 @@
diff -r 43791f99d71e -r ce1cefc6c14c Admin/page/main-content/logics.content
--- a/Admin/page/main-content/logics.content Tue Feb 13 16:05:56 2001 +0100
+++ b/Admin/page/main-content/logics.content Tue Feb 13 16:31:18 2001 +0100
@@ -79,16 +79,16 @@
-- declare concrete syntax (via mixfix grammar and syntax macros),
+
- declare concrete syntax (via mixfix grammar and syntax macros),
-
- declare abstract syntax (as higher-order constants),
+
- declare abstract syntax (as higher-order constants),
-
- declare inference rules (as meta-logical propositions),
+
- declare inference rules (as meta-logical propositions),
-
- instantiate generic automatic proof tools (simplifier, classical
+
- instantiate generic automatic proof tools (simplifier, classical
tableau prover etc.),
-
- manually code special proof procedures (via tacticals or
+
- manually code special proof procedures (via tacticals or
hand-written ML).
diff -r 43791f99d71e -r ce1cefc6c14c Admin/page/main-content/munich.content
--- a/Admin/page/main-content/munich.content Tue Feb 13 16:05:56 2001 +0100
+++ b/Admin/page/main-content/munich.content Tue Feb 13 16:31:18 2001 +0100
@@ -24,16 +24,16 @@
@@ -42,10 +42,10 @@
@@ -56,20 +56,20 @@
-- Isabelle/Bali Java and JVM
+
- Isabelle/Bali Java and JVM
formalization --- type system, semantics, compilers
-
- Isabelle/Isar Intelligible
+
- Isabelle/Isar Intelligible
semi-automated reasoning --- readable formal proof documents
- Isabelle/IOA Verification of
distributed, reactive systems using I/O Automata
-
- Isabelle/HOOL Object-oriented verification of
+
- Isabelle/HOOL Object-oriented verification of
object-oriented programs
-
- Isabelle/VerifiCard
-Tool-assisted Specification and Verification of JavaCard® Programs
+
- Isabelle/VerifiCard Tool-assisted
+Specification and Verification of JavaCard® Programs
diff -r 43791f99d71e -r ce1cefc6c14c Admin/polyml/makepkg
--- a/Admin/polyml/makepkg Tue Feb 13 16:05:56 2001 +0100
+++ b/Admin/polyml/makepkg Tue Feb 13 16:31:18 2001 +0100
@@ -4,6 +4,8 @@
SUPER="$(cd "$THIS"; cd ..; echo "$PWD")"
NAME="$(basename "$THIS")"
+[ -h "$NAME" ] && { echo "$NAME is a symlink!"; exit 2; }
+
TAR=tar
type -path gtar >/dev/null && TAR=gtar