Lines Matching defs:ma
60 e l'implicazione sono nozioni standard del calcolo dei predicati, ma la scelta �
1123 ma i dettagli sono qui omessi\footnote{La definizione delle unioni
1228 Il nome di questo valore � \holtxt{the\_value}, ma il parser e il pretty-printere sono impostati cos� che per il tipo \holtxt{$\alpha$~itself}, \holtxt{the\_value} pu� essere scritto come \holtxt{(:$\alpha$)} (la sintassi include le parentesi).
1445 contiene {\small\verb%m%} ma non {\small\verb%n%}.
1730 Su questa base, quando � eseguito il build di \HOL{} una serie \adhoc\ ma utile di pi� duecentocinquanta
1836 Le sequenze semplici di cifre sono rese dal parser come numeri decimali, ma il parser
1843 abilitati di default, ma se la reference
2052 {\small\verb+hrealTheory+}, ma non � usata una volta che i reali sono stati
2987 stessi nomi, ma con una `L\/' maiuscola anteposta. Cos�, alcune delle costanti
3138 Naturalmente, un $R$ possibile � l'eguaglianza stessa, ma la forza
3220 Il teorema per \ml{finite} ha un aspetto simile, ma ha un valore
3708 TCi sono molte altre definizioni in \theoryimp{pred\_set}, ma non sono
3711 con le altre, ma non esprimono al cun teorema profondo della teoria degli insiemi.
3770 libere, ma non c'� sovrapposizione, allora risulta un errore. L'ordine
3856 � l'insieme dei numeri da \holtxt{y} fino a ma non incluso
3876 va bene, ma questo
4147 relazione � un'istanza di $\alpha \to\alpha\to\konst{bool}$, ma la
4472 hanno il tipo $\alpha\to\beta$, ma in pi� hanno solo un numero finito di
4583 (\holtxt{DRESTRICT}), ma sufficientemente utile per essere degno di una sua propria