Searched refs:plus (Results 1 - 25 of 94) sorted by relevance

1234

/seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Tutorial/binomial/
H A Dappendix.tex22 |- !plus. Group plus ==> (!a b c. (plus b a = plus c a) ==> (b = c))
25 |- !plus times.
26 RING(plus,times) ==>
27 (!a. times(Id plus)a = Id plus) /\ (!a. times a(Id plus) = Id plus)
[all...]
H A Dbinomial.tex111 |- !plus times.
112 RING(plus,times) ==>
114 POWER times n(plus a b) =
115 SIGMA(plus,0,SUC n)(BINTERM plus times a b n))
282 # "!plus: *->*->*. ASSOCIATIVE plus =
283 # (!a b c. plus a (plus b c) = plus (plu
[all...]
/seL4-l4v-10.1.1/HOL4/Manual/Tutorial/binomial/
H A Dappendix.tex22 |- !plus. Group plus ==> (!a b c. (plus b a = plus c a) ==> (b = c))
25 |- !plus times.
26 RING(plus,times) ==>
27 (!a. times(Id plus)a = Id plus) /\ (!a. times a(Id plus) = Id plus)
[all...]
H A Dbinomial.tex111 |- !plus times.
112 RING(plus,times) ==>
114 POWER times n(plus a b) =
115 SIGMA(plus,0,SUC n)(BINTERM plus times a b n))
282 # "!plus: *->*->*. ASSOCIATIVE plus =
283 # (!a b c. plus a (plus b c) = plus (plu
[all...]
/seL4-l4v-10.1.1/l4v/tools/autocorres/tests/examples/
H A Dplus.c11 unsigned int plus(unsigned int a, unsigned int b) { function
24 return !(plus(1, 2) == plus2(1, 2));
/seL4-l4v-10.1.1/HOL4/src/quotient/Manual/
H A Dllncs.cls33 \def\thisbottomragged{\def\@textbottom{\vskip\z@ plus.0001fil
59 \setlength\textfloatsep{8mm\@plus 2\p@ \@minus 4\p@}
60 \setlength\intextsep {8mm\@plus 2\p@ \@minus 2\p@}
176 {-18\p@ \@plus -4\p@ \@minus -4\p@}%
177 {12\p@ \@plus 4\p@ \@minus 4\p@}%
179 \rightskip=\z@ \@plus 8em\pretolerance=10000 }}
181 {-18\p@ \@plus -4\p@ \@minus -4\p@}%
182 {8\p@ \@plus 4\p@ \@minus 4\p@}%
184 \rightskip=\z@ \@plus 8em\pretolerance=10000 }}
186 {-18\p@ \@plus
[all...]
/seL4-l4v-10.1.1/HOL4/src/real/
H A DrealLib.sml4 (* is also included. plus some other proof procedures. *)
H A DrealSyntax.sml86 val dest_plus = dest2 plus_tm "dest_plus" "plus"
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/src/arm/
H A Dgentramp.sh97 // This accounts for the above 4-byte stmfd instruction, plus 8 bytes constant when loading from pc.
/seL4-l4v-10.1.1/HOL4/src/res_quan/Manual/
H A Dsummacs.tex173 \def\sect{\@startsection {subsection}{1}{\z@}{-3.5ex plus -1ex minus
174 -.2ex}{1.5ex plus .2ex}{\normalsize\bf}}
175 \def\subsect{\@startsection {subsubsection}{2}{\z@}{-3.5ex plus -1ex minus
181 \parindent\z@ \parskip\z@ plus.3\p@\relax\let\item\@idxitem}{\end{multicols}}
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/ParseTree/
H A DMATCH_COMPILER.sml131 infix 3 plus;
140 fun a plus b =
143 else if first a = first b then first a ::: (next a plus next b)
144 else if first a < first b then first a ::: (next a plus b)
145 else first b ::: (a plus next b);
285 makeAot(newPatts, defaults plus singleton patNo, vars)
309 makeConsrec(cons, singleton patNo plus patts, doArg appliedTo, polyVars)
343 makeSconsrec(eqFun, cval, singleton patNo plus patts) :: ccls
394 makeExconsrec(constructor, singleton patNo plus patts, doArg appliedTo, exValue)
727 val unionSet = foldl (fn ((_, {leafSet, ...}), s) => s plus leafSe
[all...]
/seL4-l4v-10.1.1/HOL4/src/quotient/examples/
H A Dmore_listScript.sml93 (* or more equals the number of elements of value n plus the *)
/seL4-l4v-10.1.1/HOL4/src/tfl/src/
H A DRules.sml32 (* PURE_REWRITE_RULE plus generalized beta conversion. *)
/seL4-l4v-10.1.1/HOL4/src/portableML/
H A DOldPP.sig105 plus the block offset plus the offset.
/seL4-l4v-10.1.1/HOL4/polyml/basis/
H A DLibrarySupport.sml165 (* The space is the number of characters plus space for the length word
166 plus rounding. *)
/seL4-l4v-10.1.1/HOL4/examples/hardware/hol88/mos-count/
H A Dcount.ml89 % Behaviour plus proper initialization at some point %
/seL4-l4v-10.1.1/HOL4/examples/set-theory/zfset/
H A Dzfset_axiomsScript.sml8 (* (i.e. first order) ZF plus the existence of some large cardinals. *)
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/
H A DKnuthBendixOrder.sml50 (* variables in the term (plus a constant). *)
H A DRule.sig10 (* An equation consists of two terms (t,u) plus a theorem (stronger than) *)
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/
H A DKnuthBendixOrder.sml50 (* variables in the term (plus a constant). *)
H A DRule.sig10 (* An equation consists of two terms (t,u) plus a theorem (stronger than) *)
/seL4-l4v-10.1.1/HOL4/examples/dev/AES/curried/
H A DaesScript.sml2 (* Definition of the encryption and decryption algorithms plus *)
/seL4-l4v-10.1.1/HOL4/examples/dev/AES/tupled/
H A DaesScript.sml2 (* Definition of the encryption and decryption algorithms plus *)
/seL4-l4v-10.1.1/HOL4/examples/dev/AES/word8/
H A DaesScript.sml2 (* Definition of the encryption and decryption algorithms plus *)
/seL4-l4v-10.1.1/HOL4/examples/dev/sw2/
H A Dcompiler.sml98 (* All previous, plus inlining and optimizations *)

Completed in 173 milliseconds

1234