/seL4-l4v-10.1.1/HOL4/examples/real-to-float/ |
H A D | daisyLib.sml | 21 val lower = el 5 strs |> stringSyntax.fromMLstring value 23 val tm = ``rosa_correctness fp64_conf ^func 0 [(^err,^lower,^upper)]``
|
/seL4-l4v-10.1.1/seL4/src/machine/ |
H A D | io.c | 119 unsigned int upper, lower; local 131 lower = (unsigned int) x & 0xffffffff; 137 while (!(mask & lower)) { 148 n += print_unsigned_long(lower, ui_base);
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/arm/step/ |
H A D | arm_configLib.sml | 31 val lower = List.map (List.map utilsLib.lowercase) value 33 val endian_options = lower 37 val arch_options = lower 52 val vfp_options = lower
|
/seL4-l4v-10.1.1/HOL4/src/portableML/ |
H A D | smpp.sig | 26 val lower : ('st,'a) t -> 'st -> (HOLPP.pretty * 'a * 'st) option value
|
H A D | smpp.sml | 79 fun lower m st0 = function
|
/seL4-l4v-10.1.1/HOL4/polyml/basis/ |
H A D | Bool.sml | 42 (* Test for a match between a reader and a list of lower case chars. *) 48 if ch = Char.toLower ch' (* N.B. ch is already lower case. *)
|
H A D | PackWord8Big.sml | 68 fun fourBytesToWord(highest, higher, lower, low) = 71 (Word8.toLargeWord lower << 0w8) orb 74 fun fourBytesToWordX(highest, higher, lower, low) = 77 (Word8.toLargeWord lower << 0w8) orb
|
/seL4-l4v-10.1.1/HOL4/src/integer/ |
H A D | OmegaMLShadow.sml | 143 combine_dark_factoids i lower upper 443 we just need to check that the maximum of the lower bounds is less 444 than or equal to the minimum of the lower bounds. If it is then 446 false, combining the maximum lower and the minimum upper constraint. 456 fun assign_factoid (df, acc as (upper, lower)) = let 461 NONE => (SOME (fc, d), lower) 462 | SOME (c', d') => if fc < c' then (SOME (fc, d), lower) else acc 464 case lower of 466 | SOME (c', d') => if ~fc > c' then (SOME (~fc,d), lower) else acc 468 val (upper, lower) 711 val (lower, upper) = dbfold categorise (NONE, NONE) ptree value [all...] |
H A D | OmegaSimple.sig | 55 given a "lower-bound" theorem th1, and an "upper-bound" theorem
|
/seL4-l4v-10.1.1/HOL4/src/metis/ |
H A D | mlibOmega.sml | 180 combine_dark_factoids i lower upper 495 we just need to check that the maximum of the lower bounds is less 496 than or equal to the minimum of the lower bounds. If it is then 498 false, combining the maximum lower and the minimum upper constraint. 508 fun assign_factoid (df, acc as (upper, lower)) = let 513 NONE => (SOME (fc, d), lower) 514 | SOME (c', d') => if fc < c' then (SOME (fc, d), lower) else acc 516 case lower of 518 | SOME (c', d') => if ~fc > c' then (SOME (~fc,d), lower) else acc 520 val (upper, lower) 767 val (lower, upper) = dbfold categorise (NONE, NONE) ptree value [all...] |
H A D | mlibParser.sig | 57 val lower : char -> bool value
|
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/ |
H A D | depcomp | 98 { sed -e "s,^.*\.[$lower]*:,$object:," < "$tmpdepfile" 99 sed -e "s,^.*\.[$lower]*:[$tab ]*,," -e 's,$,:,' < "$tmpdepfile" 115 lower=abcdefghijklmnopqrstuvwxyz 117 alpha=${upper}${lower} 464 sed -e "s,^.*\.[$lower]*:,$object:," "$tmpdepfile" > "$depfile"
|
/seL4-l4v-10.1.1/HOL4/polyml/ |
H A D | depcomp | 98 { sed -e "s,^.*\.[$lower]*:,$object:," < "$tmpdepfile" 99 sed -e "s,^.*\.[$lower]*:[$tab ]*,," -e 's,$,:,' < "$tmpdepfile" 115 lower=abcdefghijklmnopqrstuvwxyz 117 alpha=${upper}${lower} 464 sed -e "s,^.*\.[$lower]*:,$object:," "$tmpdepfile" > "$depfile"
|
/seL4-l4v-10.1.1/isabelle/src/Doc/Logics/document/ |
H A D | syntax.tex | 24 an operator of lower priority unless brackets are used. Consider 25 first-order logic, where $\exists$ has lower priority than $\disj$, 26 which has lower priority than $\conj$. There, $P\conj Q \disj R$
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Logics/document/ |
H A D | syntax.tex | 24 an operator of lower priority unless brackets are used. Consider 25 first-order logic, where $\exists$ has lower priority than $\disj$, 26 which has lower priority than $\conj$. There, $P\conj Q \disj R$
|
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/ |
H A D | Random.sml | 30 (*NB: higher bits are more random than lower ones*)
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Random.sml | 30 (*NB: higher bits are more random than lower ones*)
|
/seL4-l4v-10.1.1/HOL4/help/src-sml/ |
H A D | ParseDoc.sml | 383 val lower = String.map Char.toLower value 384 val s1tok = lower (core_dname (Symbolic.tosymb s1)) 385 val s2tok = lower (core_dname (Symbolic.tosymb s2)) 388 EQUAL => String.compare(lower (structpart s1), lower (structpart s2))
|
/seL4-l4v-10.1.1/HOL4/src/tfl/src/test/ |
H A D | tfl_examplesScript.sml | 100 let (lower,upper) = ((ord,L1),(ord,L2)) 102 Qsort lower ++[x]++ Qsort upper)`;
|
/seL4-l4v-10.1.1/HOL4/tools/Holmake/ |
H A D | parse_glob.sml | 105 "digit", "graph", "lower", "print", "punct", 118 | ":lower:]" => return POSIX.lower_set
|
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/ |
H A D | pexport.cpp | 76 size_t lower = 0, upper = pMap.size(); local 79 ASSERT(lower < upper); 80 size_t middle = (lower+upper)/2; 84 // Use lower to middle 90 lower = middle+1;
|
/seL4-l4v-10.1.1/isabelle/src/Doc/Tutorial/document/ |
H A D | preface.tex | 20 lower-level tactics that you can use to apply rules selectively. It
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Tutorial/document/ |
H A D | preface.tex | 20 lower-level tactics that you can use to apply rules selectively. It
|
/seL4-l4v-10.1.1/HOL4/src/res_quan/Manual/ |
H A D | summacs.tex | 50 \def\DEF{\relax\ifmmode\vdash\!\!\lower .5ex\hbox{{\scriptsize\sl def}}\quad% 51 \else$\vdash\!\!\lower.5ex\hbox{{\scriptsize\sl def}}\quad$\fi}
|
/seL4-l4v-10.1.1/graph-refine/ |
H A D | inst_logic.py | 39 bit2 = bit.lower ()
|