Searched refs:right (Results 201 - 225 of 370) sorted by relevance

1234567891011>>

/seL4-l4v-10.1.1/HOL4/src/1/
H A DDrule.sml836 * Inverse of LIST_CONJ : flattens only right conjuncts. *
935 | i.e. the right-hand side is put into the antecedent. false focuses on the
936 | right hand side. If the list is empty, the equation is not splitted.
2262 ("Theorem not of right form: must be\n\
2307 ("Theorem not of right form: must be\n\
2349 ("Theorem not of right form: must be\n\
2402 ("Theorem not of right form: must be\n\
2496 the bound variable on the right is actually still an x because
H A DTypeBase.sml364 the same right-hand-side and it doesn't depend on any pattern variables.
/seL4-l4v-10.1.1/HOL4/src/integer/
H A DOmegaSymbolic.sml235 right associated
411 appropriate rewrite from OmegaTheory. The right choice of rewrite
H A DOmegaSimple.sml35 from left to right, and aren't duplicated.
/seL4-l4v-10.1.1/HOL4/src/pfl/
H A Dindex.sml352 val right = mk_is_some(dest_the rapp) value
355 val deftm = mk_eq(list_mk_comb(dom_var, args),right)
/seL4-l4v-10.1.1/HOL4/src/res_quan/src/
H A Dres_quanLib.sml135 val (left,right) = dest_conj conj
137 val right_pred = mk_abs(var,right)
H A DCond_rewrite.sml191 (* search_top_down carries out a top-down left-to-right search for *)
/seL4-l4v-10.1.1/HOL4/src/unwind/Manual/
H A Ddescription.tex372 line variable has a right-hand side of an equation associated with it. The
373 free variables in each right-hand side are computed and those that are also
/seL4-l4v-10.1.1/HOL4/tools/Holmake/
H A DHolmake_tools.sml243 if p = mypath then diag (K "In the right HOL distribution")
655 (* All files on the right of a colon are assumed to be dependencies.
H A DReadHMF.sml157 error b ("No right-paren in "^nm^" line")
/seL4-l4v-10.1.1/HOL4/tools/mlyacc/mlyacclib/
H A DMLY_parser2.sml392 let fun del(0,accum,left,right,lexPair) =
394 pos=qPos,leftPos=left,rightPos=right,
/seL4-l4v-10.1.1/HOL4/examples/ARM_security_properties/
H A DARM_proverLib.sml579 (* proof of the right part*)
592 (* combining the left and right parts *)
H A DARM_prover_extLib.sml312 (* proof of the right part*)
315 (* combining the left and right parts *)
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/src/powerpc/
H A Dlinux64_closure.S321 # ie. right justified. Larger structs are passed left justified
/seL4-l4v-10.1.1/HOL4/examples/formal-languages/regular/regular-play/src/
H A DregexMarkedScript.sml334 (* recursively, m says whether to start, c says what to match, this should be right for all marks that are already there and the virtual mark m *)
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/extra/Win/
H A DMetafile.sml24 type RECT = { top: int, left: int, bottom: int, right: int }
H A DClipboard.sml142 right form of subclassing to allow all the various handle types to be combined. *)
/seL4-l4v-10.1.1/HOL4/src/coretypes/
H A DPairedLambda.sml211 (* the right-hand side of the input theorem th, at the places that *)
H A DpairSyntax.sml59 in left-to-right order.
/seL4-l4v-10.1.1/HOL4/src/portableML/poly/
H A DIntset.sml107 if rn>=wt ln then (*right is too big*)
/seL4-l4v-10.1.1/HOL4/src/real/
H A DhratScript.sml310 (* Save theorems and make sure they are all of the right form *)
/seL4-l4v-10.1.1/HOL4/src/simp/src/
H A DTraverse.sml168 (* This code is used just once, to do the right thing with the
H A DboolSimps.sml365 * - inwards into right of implications
/seL4-l4v-10.1.1/HOL4/examples/HolCheck/examples/
H A Damba_ahb.sml127 (* default master always the bus upon request (either right away, or if masked then after demasking via hsplit) *)
/seL4-l4v-10.1.1/HOL4/examples/HolCheck/
H A DstringBinTree.sml50 fun rmid L = List.nth(L,(List.length L) div 2); (* return middle or right middle element *)

Completed in 326 milliseconds

1234567891011>>