/seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Tutorial/binomial/ |
H A D | appendix.tex | 22 |- !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 D | binomial.tex | 111 |- !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 D | appendix.tex | 22 |- !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 D | binomial.tex | 111 |- !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 D | plus.c | 11 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 D | llncs.cls | 33 \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 D | realLib.sml | 4 (* is also included. plus some other proof procedures. *)
|
H A D | realSyntax.sml | 86 val dest_plus = dest2 plus_tm "dest_plus" "plus"
|
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/src/arm/ |
H A D | gentramp.sh | 97 // 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 D | summacs.tex | 173 \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 D | MATCH_COMPILER.sml | 131 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 D | more_listScript.sml | 93 (* or more equals the number of elements of value n plus the *)
|
/seL4-l4v-10.1.1/HOL4/src/tfl/src/ |
H A D | Rules.sml | 32 (* PURE_REWRITE_RULE plus generalized beta conversion. *)
|
/seL4-l4v-10.1.1/HOL4/src/portableML/ |
H A D | OldPP.sig | 105 plus the block offset plus the offset.
|
/seL4-l4v-10.1.1/HOL4/polyml/basis/ |
H A D | LibrarySupport.sml | 165 (* 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 D | count.ml | 89 % Behaviour plus proper initialization at some point %
|
/seL4-l4v-10.1.1/HOL4/examples/set-theory/zfset/ |
H A D | zfset_axiomsScript.sml | 8 (* (i.e. first order) ZF plus the existence of some large cardinals. *)
|
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/ |
H A D | KnuthBendixOrder.sml | 50 (* variables in the term (plus a constant). *)
|
H A D | Rule.sig | 10 (* 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 D | KnuthBendixOrder.sml | 50 (* variables in the term (plus a constant). *)
|
H A D | Rule.sig | 10 (* 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 D | aesScript.sml | 2 (* Definition of the encryption and decryption algorithms plus *)
|
/seL4-l4v-10.1.1/HOL4/examples/dev/AES/tupled/ |
H A D | aesScript.sml | 2 (* Definition of the encryption and decryption algorithms plus *)
|
/seL4-l4v-10.1.1/HOL4/examples/dev/AES/word8/ |
H A D | aesScript.sml | 2 (* Definition of the encryption and decryption algorithms plus *)
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw2/ |
H A D | compiler.sml | 98 (* All previous, plus inlining and optimizations *)
|