| /seL4-l4v-10.1.1/HOL4/examples/elliptic/ |
| H A D | Useful.sml | 175 fun pair x y = (x,y); function
189 val unit : 'a -> 's -> 'a * 's = pair;
246 fun zip xs ys = zipwith pair xs ys;
262 fun cart xs ys = cartwith pair xs ys;
|
| /seL4-l4v-10.1.1/HOL4/src/HolSat/ |
| H A D | minisatResolve.sml | 34 (* clauseth[i] gives i'th clause of CNF, as a pair (t,[tm] |- t') *)
|
| /seL4-l4v-10.1.1/HOL4/src/coretypes/ |
| H A D | pairLib.sml | 75 raise pairLib_ERR "strip_pair_case" "not a pair case"
|
| H A D | PairRules.sml | 163 (* pairlike p x: takes a pair structure p and a term x. *)
236 (* instances of the bound pair p and it subcomponents. *)
450 (* If the argument of the resulting conversion is a pair, this conversion *)
451 (* recursively applies itself to both sides of the pair. *)
782 failwith "bound pair occurs in both conjuncts"
931 failwith "bound pair occurs in both conjuncts"
1098 failwith "bound pair occurs in both sides of `==>`"
1237 failwith "bound pair occurs in both sides of `==>`"
1987 raise ERR"P_SKOLEM_CONV" "first argument not a variable pair"
2016 "existential variable not of pair typ
[all...] |
| H A D | PairedLambda.sml | 86 local val pair = CONV_RULE (ONCE_DEPTH_CONV SYM_CONV) pairTheory.PAIR value
95 val eqv = if can dest_pair arg then REFL arg else ISPEC arg pair
|
| /seL4-l4v-10.1.1/HOL4/src/marker/ |
| H A D | markerScript.sml | 54 (* Note, if you want to move a pair of things to the edge of a term,
|
| /seL4-l4v-10.1.1/HOL4/src/postkernel/ |
| H A D | HolKernel.sml | 40 val (c1, pair) = with_exn dest tm e
42 if same_const c c1 then pair else raise e
92 val ({Name, Thy, ...}, pair) = with_exn dest tm e
94 if Name = name andalso Thy = thy then pair else raise e
|
| /seL4-l4v-10.1.1/HOL4/src/prekernel/ |
| H A D | Tag.sml | 18 (* A tag is represented by a pair (D,O,A) where O is a list of oracles *)
|
| /seL4-l4v-10.1.1/HOL4/src/tactictoe/src/ |
| H A D | tttOpen.sml | 22 "one", "sum", "option", "pair", "combin", "sat", "normalForms",
|
| /seL4-l4v-10.1.1/isabelle/src/Pure/Isar/ |
| H A D | token.scala | 257 pair(int, string)(tok.kind.id, tok.source)
263 val (k, s) = pair(int, string)(body)
|
| /seL4-l4v-10.1.1/isabelle/src/Pure/PIDE/ |
| H A D | markup.scala | 666 pair(string, properties)((markup.name, markup.properties))
672 val (name, props) = pair(string, properties)(body)
|
| /seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/ |
| H A D | Map.sig | 41 val pick : ('key,'a) map -> 'key * 'a (* an arbitrary key/value pair *)
|
| H A D | Useful.sig | 55 val pair : 'a -> 'b -> 'a * 'b value
|
| H A D | Useful.sml | 103 fun pair x y = (x,y); function
117 val unit : 'a -> 's -> 'a * 's = pair;
219 fun zip xs ys = zipWith pair xs ys;
238 fun cart xs ys = cartwith pair xs ys;
|
| /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/l4v/isabelle/src/Pure/Isar/ |
| H A D | token.scala | 257 pair(int, string)(tok.kind.id, tok.source)
263 val (k, s) = pair(int, string)(body)
|
| /seL4-l4v-10.1.1/l4v/isabelle/src/Pure/PIDE/ |
| H A D | markup.scala | 666 pair(string, properties)((markup.name, markup.properties))
672 val (name, props) = pair(string, properties)(body)
|
| /seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/ |
| H A D | Map.sig | 41 val pick : ('key,'a) map -> 'key * 'a (* an arbitrary key/value pair *)
|
| H A D | Useful.sig | 55 val pair : 'a -> 'b -> 'a * 'b value
|
| H A D | Useful.sml | 103 fun pair x y = (x,y); function
117 val unit : 'a -> 's -> 'a * 's = pair;
219 fun zip xs ys = zipWith pair xs ys;
238 fun cart xs ys = cartwith pair xs ys;
|
| /seL4-l4v-10.1.1/HOL4/src/HolQbf/ |
| H A D | QbfLibrary.sml | 20 List.app (TextIO.output o Lib.pair outstream) strings;
91 (* pair consisting of a positive integer i and a Boolean q, and a *)
|
| /seL4-l4v-10.1.1/HOL4/src/metis/ |
| H A D | metisTools.sml | 59 | bool_map "pair.FST" = SOME "id"
60 | bool_map "pair.," = SOME "fst"
|
| /seL4-l4v-10.1.1/HOL4/examples/ARM/v7/ |
| H A D | arm_coretypesScript.sml | 480 ["pair.UNCURRY",
481 "pair.LEX_DEF",
|
| /seL4-l4v-10.1.1/HOL4/examples/ARM_security_properties/model/ |
| H A D | arm_coretypesScript.sml | 484 ["pair.UNCURRY",
485 "pair.LEX_DEF",
|
| /seL4-l4v-10.1.1/HOL4/examples/Crypto/RC6/ |
| H A D | RC6Script.sml | 133 (* Rotate keys and get a pair of keys from the head of the key schedule *)
200 (* that PreWhitening and PostWhitening use the same key pair *)
|