Searched refs:cal (Results 1 - 8 of 8) sorted by relevance

/seL4-l4v-10.1.1/HOL4/Manual/Logic/
H A Dsemantics.tex86 \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 Dsyntax.tex34 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 Dsemantics.tex86 \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 Dsyntax.tex34 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 Dselftest.sml58 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 Dsystem.tex879 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 Ddrules.tex6 $\Delta$ (rispetto a un sistema deduttivo ${\cal D}$) �
/seL4-l4v-10.1.1/HOL4/src/pred_set/src/
H A Dpred_setScript.sml377 val _ = TeX_notation {hol = "univ", TeX = ("\\ensuremath{\\cal{U}}", 1)}
379 TeX = ("\\ensuremath{\\cal{U}}", 1)}

Completed in 79 milliseconds