aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/g_vernacnew.ml4
Commit message (Expand)AuthorAge
* Ajout V8NotationGravatar herbelin2003-05-22
* Possibilité de syntaxe conjointement à la définition des inductifs et des ...Gravatar herbelin2003-05-21
* Prise en compte des syntaxes v8 dans Uninterpreted NotationGravatar herbelin2003-04-29
* Factorisation des produits de même type; parenthèses autour des x:=c et n:=...Gravatar herbelin2003-04-29
* Ajout "at next level" dans NotationGravatar herbelin2003-04-17
* Ajout option 'Local' à Infix et NotationGravatar herbelin2003-04-11
* Ajout option "Local" à "Open Scope"Gravatar herbelin2003-04-08
* Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar)Gravatar herbelin2003-03-29
* MAJ des mots-clés, Definition, Theorem, ...Gravatar herbelin2003-03-27
* *** empty log message ***Gravatar barras2003-03-21
* *** empty log message ***Gravatar barras2003-03-12