X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FsearchEngine%2Fhtml%2Fexpr.html;h=dea29bc52a8a9a93eab408b37a6e30f9fc9426ff;hb=25bcb9af3fc3ce3cebd369e3cd9f3a704403a173;hp=3e302b8b24fc366fed1119c6803856acbdd6c35d;hpb=02f84dc4ebb39cbebcaac6d2bbbf1e8413e10aa1;p=helm.git diff --git a/helm/searchEngine/html/expr.html b/helm/searchEngine/html/expr.html index 3e302b8b2..dea29bc52 100644 --- a/helm/searchEngine/html/expr.html +++ b/helm/searchEngine/html/expr.html @@ -5,12 +5,13 @@ function choice() { with (document.form1) { stadd="";top.qw.document.close();quanti=0; - if (selopt[0].checked) {stadd="\[Genid]"+document.form1.ex1.value+"[Expr].[Expr]"} - if (selopt[1].checked) {stadd="![Genid]:[Expr].[Expr]"} - if (selopt[2].checked) {stadd="[Expr]->[Expr]"} - if (selopt[3].checked) {stadd="([Expr])->[Expr]"} - if (selopt[4].checked) {stadd=document.form1.ex2.value} - if (selopt[5].checked) { + if (selopt[0].checked) {stadd="\\lambda [Genid] : [Expr].[Expr]"} + if (selopt[1].checked) {stadd="let [Genid] = [Expr] in [Expr]"} + if (selopt[2].checked) {stadd="\\forall [Genid]:[Expr].[Expr]"} + if (selopt[3].checked) {stadd="[Expr] \\to [Expr]"} + if (selopt[4].checked) {stadd="?"} + if (selopt[5].checked) {stadd=document.form1.ex2.value} + if (selopt[6].checked) { while (quanti<1) { quanti=prompt("How many expressions in the list?","1");//alert(quanti); @@ -21,7 +22,7 @@ with (document.form1) { {stadd=stadd+"[Expr] "} stadd=stadd+")"; } - if (selopt[6].checked) { + if (selopt[7].checked) { stadd=document.form1.id_or_uri.value; //alert(stadd.substring(0,5)); if (stadd.substring(0,5)=="cic:/") @@ -39,13 +40,11 @@ with (document.form1) { You are entering an expression. Select one of the following.
-\[Genid][Expr].[Expr]
-![Genid]:[Expr].[Expr]
-[Expr]->[Expr]
-([Expr])->[Expr]
+\lambda [Genid]:[Expr].[Expr]
+let [Genid] = [Expr] in [Expr]
+\forall [Genid]:[Expr].[Expr]
+[Expr] \to [Expr]
+?
- \ No newline at end of file +