| /seL4-l4v-10.1.1/HOL4/src/tfl/src/ |
| H A D | RW.sml | 444 * Takes a list of free variables and a list of pairs. If any of
445 * the free variables are in the pairs, they are replaced in the pairs
446 * by variants. The final pairs are returned.
636 (* val pairs = zip args vstructs' handle HOL_ERR _ => [] *)
637 val pairs = zip args vstructs handle HOL_ERR _ => [] value
639 case assoc1 v pairs
|
| /seL4-l4v-10.1.1/HOL4/src/bag/ |
| H A D | bagSimpleLib.sml | 263 (* destructs these bags and searches for pairs of elements that satisfy *)
265 (* the positions of the found pairs. These lists are suitable to be given to *)
266 (* BAG_RESORT_CONV. This function is useful to find pairs and sort them to *)
|
| /seL4-l4v-10.1.1/HOL4/src/HolSat/ |
| H A D | satTools.sml | 20 ** and DIMACS variable numbers as a set of string*int pairs.
|
| H A D | dpll.sml | 91 fun doCNF neg_tm = (* clauses is (ci,[~t] |- ci') pairs, where ci' is expanded ci *)
|
| /seL4-l4v-10.1.1/HOL4/src/integer/ |
| H A D | jrhUtils.sml | 45 (* GEN_PAIR_TAC - Like GEN_TAC but "pairs" the relevant variable *)
|
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/graph/ |
| H A D | backgroundLib.sml | 83 (* expands pairs ``(x,y,z) = f`` --> (x = FST f) /\ (y = FST (SND f)) /\ (z = ...) *)
|
| /seL4-l4v-10.1.1/HOL4/examples/acl2/examples/LTL/ |
| H A D | COIRScript.sml | 71 * The equations are represented by a set of pairs (v,e) where v is a
|
| /seL4-l4v-10.1.1/HOL4/polyml/basis/ |
| H A D | List.sml | 105 (* TODO: This involves returning a pair and creating new pairs
|
| /seL4-l4v-10.1.1/HOL4/src/coretypes/ |
| H A D | PairedLambda.sml | 2 Raising basic lambda calculus conversions to handle pairs
292 (* to handle values that are not explicitly pairs *)
|
| /seL4-l4v-10.1.1/isabelle/src/Doc/Tutorial/document/ |
| H A D | sets.tex | 6 regard a relation as a set of pairs. The chapter introduces the well-known
646 A \textbf{relation} is a set of pairs. As such, the set operations apply
841 of a subtle issue involving ordered pairs. Here is a subgoal that
853 ordered pairs, while \isa{x} is a variable of product type.
863 techniques for ordered pairs in more detail.
901 that is, a set of pairs of natural numbers. Two theorems tell us that this
938 standard dictionary ordering over pairs. We write \isa{ra\ <*lex*>\
|
| /seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Tutorial/document/ |
| H A D | sets.tex | 6 regard a relation as a set of pairs. The chapter introduces the well-known
646 A \textbf{relation} is a set of pairs. As such, the set operations apply
841 of a subtle issue involving ordered pairs. Here is a subgoal that
853 ordered pairs, while \isa{x} is a variable of product type.
863 techniques for ordered pairs in more detail.
901 that is, a set of pairs of natural numbers. Two theorems tell us that this
938 standard dictionary ordering over pairs. We write \isa{ra\ <*lex*>\
|
| /seL4-l4v-10.1.1/HOL4/src/num/arith/src/ |
| H A D | Norm_arith.sml | 121 (* Takes an association list of pairs of integers, and theorems about the *)
122 (* simplification of the products of the pairs of integers. The second *)
|
| /seL4-l4v-10.1.1/HOL4/src/opentheory/postbool/ |
| H A D | Opentheory.sml | 223 | _ => raise ERR "subst failed to pop a list of [name,type] pairs") tys
225 | _ => raise ERR "subst failed to pop a list of [var,term] pairs") tms
|
| /seL4-l4v-10.1.1/HOL4/tools/Holmake/ |
| H A D | regexpMatch.sml | 235 val pairs = cross (listItems class1) (listItems class2) value
240 pairs
|
| /seL4-l4v-10.1.1/HOL4/examples/HolCheck/ |
| H A D | commonTools.sml | 201 (* destroy linear nested conditional, returning (test,true branch) pairs (the last false branch is dropped) *)
209 (* destroy general conditional, returning (list of tests,value) pairs *)
|
| H A D | envTools.sml | 28 (* rvl: list of (rel var:string,corresponding boolean term for state set:bool) pairs
|
| /seL4-l4v-10.1.1/HOL4/examples/imperative/ |
| H A D | reflectOnFailure.sml | 70 The left-hand spec pairs these states up and returns true if either the input state does not apply, or the output
|
| /seL4-l4v-10.1.1/HOL4/examples/ind_def/ |
| H A D | algebraScript.sml | 274 (* also be done by Q such that the corresponding successive pairs of *)
|
| /seL4-l4v-10.1.1/HOL4/src/quantHeuristics/ |
| H A D | quantHeuristicsLibAbbrev.sml | 184 (* For pairs, the pattern "(\(x,y). P) X" is useful as well *)
|
| H A D | quantHeuristicsLibParameters.sml | 37 file contains heuristics for common construcs like lists, pairs,
|
| /seL4-l4v-10.1.1/HOL4/Manual/Description/ |
| H A D | QuantHeuristics.tex | 112 \texttt{std\_qp} adds support for common datatypes like pairs or lists.
251 However, it supports more complicated syntax. Moreover, there is support for quantifiers, pairs, list and much more.
305 Records are similar to pairs, because they can always be instantiated. Here, it is interesting that the necessary
328 for pairs and the default one for records.
|
| /seL4-l4v-10.1.1/HOL4/developers/discussion/ |
| H A D | overloading-extension.tex | 133 really one from name-type pairs to lists of the same.
|
| /seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/CodeTree/ |
| H A D | BaseCodeTreeSig.sml | 140 offset to one of these pairs; inline function entries are a
|
| /seL4-l4v-10.1.1/isabelle/src/Doc/Intro/document/ |
| H A D | root.tex | 24 \newcommand\qeq{\stackrel{?}{\equiv}} %for disagreement pairs in unification
|
| /seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Intro/document/ |
| H A D | root.tex | 24 \newcommand\qeq{\stackrel{?}{\equiv}} %for disagreement pairs in unification
|