Searched refs:cal (Results 1 - 8 of 8) sorted by relevance
/seL4-l4v-10.1.1/HOL4/Manual/Logic/ |
H A D | semantics.tex | 86 \prod_{X\!s\in{\cal U}^{n}} \left( 93 if for all $X\!s\in{\cal U}^{n}$ and 108 \den{t}_M \in \prod_{X\!s\in{\cal U}^{n}} 116 ${\cal D}$ is a set of pairs $(L,(\Gamma,t))$ where $L$ is a 122 ${\cal D}$ if 131 \item $(L_i,(\Gamma_i,t_i))\in{\cal D}$ for some list $L_i$ of members of 137 $(\Gamma,t)$ from $\Delta$ with respect to ${\cal D}$. 143 The notation\index{turnstile notation} $t_1,\ldots,t_n\vdash_{{\cal 145 follows from $\Delta$ by ${\cal D}$. If either ${\cal [all...] |
H A D | syntax.tex | 34 terms of a fixed set of sets $\cal U$, which will be called the {\em 40 \item[Inhab] Each element of $\cal U$ is a non-empty set. 42 \item[Sub] If $X\in{\cal U}$ and $\emptyset\not=Y\subseteq X$, then 43 $Y\in{\cal U}$. 45 \item[Prod] If $X\in{\cal U}$ and $Y\in{\cal U}$, then $X\times 46 Y\in{\cal U}$. The set $X\times Y$ is the cartesian product, 51 \item[Pow] If $X\in{\cal U}$, then the powerset 52 $P(X)=\{Y:Y\subseteq X\}$ is also an element of $\cal U$. 54 \item[Infty] $\cal [all...] |
/seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Logic/ |
H A D | semantics.tex | 86 \prod_{X\!s\in{\cal U}^{n}} \left( 93 se per tutti gli $X\!s\in{\cal U}^{n}$ e 108 \den{t}_M \in \prod_{X\!s\in{\cal U}^{n}} 116 ${\cal D}$ � un insieme di coppie $(L,(\Gamma,t))$ dove $L$ � una 122 ${\cal D}$ se 131 \item $(L_i,(\Gamma_i,t_i))\in{\cal D}$ per qualche lista $L_i$ di membri di 137 $(\Gamma,t)$ da $\Delta$ rispetto a ${\cal D}$. 143 La notazione\index{turnstile} $t_1,\ldots,t_n\vdash_{{\cal 145 segue da $\Delta$ per ${\cal D}$. Se o ${\cal [all...] |
H A D | syntax.tex | 34 termini di un insieme di insiemi fisso $\cal U$, che sar� chiamato l'{\em 40 \item[Inhab] Ogni elemento di $\cal U$ � un insieme non vuoto. 42 \item[Sub] Se $X\in{\cal U}$ e $\emptyset\not=Y\subseteq X$, allora 43 $Y\in{\cal U}$. 45 \item[Prod] Se $X\in{\cal U}$ e $Y\in{\cal U}$, allora $X\times 46 Y\in{\cal U}$. L'insieme $X\times Y$ � il prodotto cartesiano, 51 \item[Pow] Se $X\in{\cal U}$, allora anche l'insieme potenza 52 $P(X)=\{Y:Y\subseteq X\}$ � un elemento di $\cal U$. 54 \item[Infty] $\cal [all...] |
/seL4-l4v-10.1.1/HOL4/src/TeX/ |
H A D | selftest.sml | 58 val _ = if s = "\\ensuremath{\\cal{U}}(:'a)" then OK() else gotdie s 64 val _ = if s = "\\ensuremath{\\cal{U}}(:\\ensuremath{\\alpha})" then OK() 69 val _ = if s = "\\ensuremath{\\cal{U}}(:\\HOLTyOp{num})" then OK()
|
/seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Description/ |
H A D | system.tex | 879 insieme di sequenti $\Delta$, attraverso un sistema deduttivo ${\cal D}$, � 880 denotato da: $t_1,\ldots,t_n\vdash_{{\cal D},\Delta} t$. (E' stato notato 881 che dove sia ${\cal D}$ sia $\Delta$ sono fossero chiari dal contesto, la loro 1444 \[ {\cal T}\ =\ \langle{\sf Struc}_{\cal T},\ 1445 {\sf Sig}_{\cal T},\ 1446 {\sf Axioms}_{\cal T},\ 1447 {\sf Theorems}_{\cal T}\rangle \] 1451 \item ${\sf Struc}_{\cal T}$ � 1452 la struttura di tipo di ${\cal [all...] |
H A D | drules.tex | 6 $\Delta$ (rispetto a un sistema deduttivo ${\cal D}$) �
|
/seL4-l4v-10.1.1/HOL4/src/pred_set/src/ |
H A D | pred_setScript.sml | 377 val _ = TeX_notation {hol = "univ", TeX = ("\\ensuremath{\\cal{U}}", 1)} 379 TeX = ("\\ensuremath{\\cal{U}}", 1)}
|
Completed in 79 milliseconds