additions to basic_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
    </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
    </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
          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"/>
 
    </body>
    <table name="apps_2_src"/>