X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambda_delta%2Fweb%2Fhome%2Fapps_2.ldw.xml;h=2d15c0bf705f7ced89d868615820c4a0309847c2;hb=0fa1d4541bec571d84c726c488ba500a269bfb07;hp=253fbdc876e089674d1cfab9d436eb4b008b0614;hpb=ae7427e8d3c57ccc77931e27913d8605d385cbda;p=helm.git 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 253fbdc87..2d15c0bf7 100644 --- 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 @@ Martin-Löf's Type Theory with one universe - using λδ as the theory of expressions. + using λδ as theory of expressions. 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).