Searched defs:mt (Results 1 - 10 of 10) sorted by relevance

/seL4-l4v-master/HOL4/examples/ARM/arm6-verification/
H A DarmLib.sml109 val mt = get_abbrev_match m t value
/seL4-l4v-master/HOL4/examples/ARM/v4/
H A DarmLib.sml94 val mt = get_abbrev_match m t value
H A Darm_rulesLib.sml91 val mt = get_abbrev_match m t value
/seL4-l4v-master/HOL4/src/compute/src/
H A Dclauses.sml213 | NONE => let val mt = ref (EndDb, NONE) value
/seL4-l4v-master/HOL4/src/floating-point/
H A Dbinary_ieeeLib.sml98 val mt = Arbnum.less1 (dimword t) value
/seL4-l4v-master/HOL4/examples/theorem-prover/lisp-runtime/extract/
H A Dlisp_extractLib.sml400 val mt = dest_term t value
467 val mt = dest_term t value
735 val mt = dest_term t value
910 val mt = dest_term t value
/seL4-l4v-master/HOL4/src/real/
H A DrealSimps.sml1006 val mt = Arbint.*(ld,rd) |> term_of_int value
/seL4-l4v-master/HOL4/examples/acl2/ml/
H A DencodeLib.sml1742 val mt = first (not o C (exists_coding_theorem target) "decode_encode_fix") (all_types t) value
1788 val mt = first (not o C (exists_coding_theorem target) "fix_id" o base_type) all_types value
H A DfunctionEncodeLib.sml234 val mt = fst (dom_rng (type_of a)) value
/seL4-l4v-master/HOL4/examples/l3-machine-code/riscv/model/
H A Driscv.sml2060 val mt = ref orig value
2108 val mt = ref (rec'mstatus(reg'mstatus mst)) value
[all...]

Completed in 300 milliseconds