update in basic_2 and apps_2

[helm.git] / helm / www / lambda_delta / web / home / apps_2.ldw.xml

diff --git a/helm/www/lambda_delta/web/home/apps_2.ldw.xml b/helm/www/lambda_delta/web/home/apps_2.ldw.xml
index 253fbdc876e089674d1cfab9d436eb4b008b0614..2d15c0bf705f7ced89d868615820c4a0309847c2 100644 (file)
--- a/helm/www/lambda_delta/web/home/apps_2.ldw.xml
+++ b/helm/www/lambda_delta/web/home/apps_2.ldw.xml
@@ -12,7 +12,7 @@
    </body>
    <news date="MLTT1.">
          Martin-Löf's Type Theory with one universe
-        using λδ as the theory of expressions.
+        using λδ as theory of expressions.
    </news>
    <news date="Functional.">
          The validation algorithm for λδ as implemented in
@@ -40,7 +40,7 @@
          according to the following table.
          Each component contains its own notation file.
         The notation for the relations or functions introduced in each file
-        is shown in parentheses.
+        is shown in parentheses (? are placeholders).
    </body>
    <table name="apps_2_src"/>