# HG changeset patch
# User paulson
# Date 826039621 -3600
# Node ID c81c770f47efa68905d5fc5cd4716d0d3cd5c400
# Parent eacaa07e907809deae42cf7f3ae897edf9acf406
Put quotes around URLs in links
diff -r eacaa07e9078 -r c81c770f47ef src/HOL/Lambda/README.html
--- a/src/HOL/Lambda/README.html Tue Mar 05 15:55:15 1996 +0100
+++ b/src/HOL/Lambda/README.html Tue Mar 05 16:27:01 1996 +0100
@@ -1,4 +1,4 @@
-HOL/Lambda/ReadMe
+HOL/Lambda
Lambda Calculus in de Bruijn's Notation
@@ -8,9 +8,10 @@
-A report describing the whole theory is found here:
-
-More Church-Rosser Proofs (in Isabelle/HOL).
+The report
+
+More Church-Rosser Proofs (in Isabelle/HOL)
+describes the whole theory.
diff -r eacaa07e9078 -r c81c770f47ef src/ZF/IMP/README.html
--- a/src/ZF/IMP/README.html Tue Mar 05 15:55:15 1996 +0100
+++ b/src/ZF/IMP/README.html Tue Mar 05 16:27:01 1996 +0100
@@ -1,6 +1,7 @@
-
HOL/IMP/ReadMe
+
+HOL/IMP
-IMP --- A while-language and two semantics
+IMP -- A while-language and two semantics
The formalization of the denotational and operational semantics of
a simple while-language together with an equivalence proof between the two
@@ -15,10 +16,14 @@
year = 1993}.
-Some documentation is found
-
-here
+There is a
+
+report by Lötzbeyer and Sandner.
A much extended version of this development is found in
-HOL/IMP.
+HOL/IMP.
+
+
+
+Last modified 5 March 1996