| /seL4-l4v-10.1.1/HOL4/src/prekernel/ |
| H A D | Nonce.sig | 5 val mk : 'a -> 'a t value
|
| H A D | Nonce.sml | 5 fun mk v = ref v function
|
| /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/lib/ |
| H A D | Set.sig | 13 val mk : ''a list -> ''a list value
|
| H A D | Set.sml | 12 fun mk [] = [] function
|
| /seL4-l4v-10.1.1/HOL4/examples/formal-languages/context-free/ |
| H A D | pegML.sml | 122 val mk = map str o explode value
|
| /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/common/ |
| H A D | temporal_stateSyntax.sml | 32 val mk = HolKernel.list_mk_icomb (if b then tm2 else tm1) value
|
| H A D | Import.sml | 466 val mk = if listSyntax.is_list_type (Term.type_of lst) value
|
| /seL4-l4v-10.1.1/HOL4/src/bool/ |
| H A D | TexTokenMap.sml | 28 val (mk,dest) = Theory.LoadableThyData.new value
|
| /seL4-l4v-10.1.1/HOL4/src/num/arith/src/ |
| H A D | GenRelNorm.sml | 7 val mk : term * term -> term value
|
| H A D | NumRelNorms.sml | 128 val mk = mk_plus value
|
| /seL4-l4v-10.1.1/HOL4/src/1/ |
| H A D | ThmSetData.sml | 91 val (mk,dest) = LoadableThyData.new {merge = set_alist_merge, value
136 val (mk,dest) = new name value
[all...] |
| H A D | boolSyntax.sml | 456 fun mk n = prim_mk_const {Name = n, Thy = "bool"} function
|
| H A D | selftest.sml | 602 fun mk i = if i = ai then mk_comb(mk_abs(B 0,B 0), B (jump ti i)) function
|
| H A D | Pmatch.sml | 348 fun mk{rows=[],...} = mk_case_fail "no rows" function
[all...] |
| /seL4-l4v-10.1.1/HOL4/src/floating-point/ |
| H A D | machine_ieeeScript.sml | 112 fun mk s = Term.prim_mk_const {Name = "fp64_" ^ s, Thy = "machine_ieee"} function
[all...] |
| /seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/ |
| H A D | Clause.sig | 37 val mk : clauseInfo -> clause value
|
| H A D | Clause.sml | 75 fun mk info = Clause info function
|
| /seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/ |
| H A D | Clause.sig | 37 val mk : clauseInfo -> clause value
|
| H A D | Clause.sml | 75 fun mk info = Clause info function
|
| /seL4-l4v-10.1.1/HOL4/src/opentheory/ |
| H A D | OpenTheoryMap.sml | 57 val (mk,dest) = value
|
| /seL4-l4v-10.1.1/HOL4/src/real/ |
| H A D | realaxScript.sml | 155 fun mk ts = mk_binop itm (list_mk_binop ts) function
|
| /seL4-l4v-10.1.1/HOL4/src/basicProof/ |
| H A D | BasicProvers.sml | 977 val {mk,dest,export} = value
|
| /seL4-l4v-10.1.1/HOL4/src/n-bit/ |
| H A D | blastLib.sml | 533 fun mk (sgn, p) = function
|
| /seL4-l4v-10.1.1/HOL4/src/tfl/src/ |
| H A D | Induction.sml | 195 fun mk{rows=[],...} = fail"no rows" function
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/x64/step/ |
| H A D | x64_stepLib.sml | 1000 val mk = value
|