| /seL4-l4v-10.1.1/HOL4/src/HolQbf/ |
| H A D | HolQbfLib.sml | 10 val dict = QDimacs.write_qdimacs_file path t value
34 val (dict, cert) = get_certificate t value
48 val (dict, cert) = get_certificate t value
64 val (dict, cert) = get_certificate t value
82 val (dict, cert) = get_certificate t' value
[all...] |
| H A D | selftest.sml | 34 val dict = QDimacs.write_qdimacs_file path t value
|
| H A D | QDimacs.sml | 45 val dict = ref (Redblackmap.mkDict Term.compare) value
|
| /seL4-l4v-10.1.1/HOL4/src/finite_map/ |
| H A D | flookupLib.sml | 219 val (dict, rest) = value
226 val dict = Redblackmap.transform rule dict value
[all...] |
| /seL4-l4v-10.1.1/HOL4/src/postkernel/ |
| H A D | ThyDataSexp.sml | |
| /seL4-l4v-10.1.1/HOL4/src/opentheory/postbool/ |
| H A D | Opentheory.sml | 219 val (dict, value
[all...] |
| H A D | Logging.sml | 113 val dict = ref (new_dict()) value
|
| /seL4-l4v-10.1.1/HOL4/src/HolSmt/ |
| H A D | Yices.sml | 458 val (dict, fresh, ty_dict, ty_fresh, defs) = acc value
482 val dict = union dict (diff body_dict bound_dict) value
499 val (dict, fresh, ty_dict, ty_fresh, defs) = acc' value
519 val (dict, fresh, ty_dict, ty_fresh, defs) = acc value
681 let val (dict, fresh, ty_dict, ty_fresh, defs) = acc value
687 val dict = Redblackmap.insert (dict, tm, name) value
[all...] |
| H A D | Z3_ProofReplay.sml | 124 val dict = disjuncts (Redblackmap.mkDict Term.compare) (t, Thm.ASSUME t) value
126 val dict = List.foldl (fn (th, dict) value
143 val dict = Redblackmap.insert value
268 val dict = Redblackmap.insert (dict, t, th) value
280 val dict = Redblackmap.insert (dict, Thm.concl th1, th1) value
311 val dict = disjuncts (Redblackmap.mkDict Term.compare) (Lib.I, disj) value
313 val dict = Redblackmap.insert (dict, boolSyntax.T, boolTheory.TRUTH) value
457 val (dict, l) = aux (dict, l) value
458 val (dict, r) = aux (dict, r) value
835 val (dict, t') = generalize_ite t value
[all...] |
| /seL4-l4v-10.1.1/HOL4/src/quotient/examples/sigma/ |
| H A D | barendregt.sml | 67 val dict = ty_antiq( ==`:(string # method) list`== ); value
|
| H A D | semanticsScript.sml | 39 val dict = ty_antiq( ==`:(string # method) list`== ); value
[all...] |
| H A D | liftScript.sml | 36 val dict = ty_antiq( ==`:(string # method1) list`== ); value
1627 val dict = ty_antiq( ==`:(string # method) list`== ); value
[all...] |
| H A D | reductionScript.sml | 35 val dict = ty_antiq( ==`:(string # method) list`== ); value
[all...] |
| /seL4-l4v-10.1.1/HOL4/src/tactictoe/src/ |
| H A D | tacticToe.sml | 98 val dict = dnew String.compare feav value
|
| H A D | tttPredict.sml | 22 val dict = count_dict (dempty Int.compare) syms value
168 val dict = ref thmdict value
[all...] |
| /seL4-l4v-10.1.1/HOL4/src/holyhammer/ |
| H A D | hhTranslate.sml | 300 val dict = ref (dempty String.compare) value
|
| H A D | hhWriter.sml | 74 let val dict = #used_names state in value
83 val dict = #ty_names state value
95 val dict = #const_names state value
107 val dict = #thm_names state value
[all...] |
| H A D | holyHammer.sml | 113 val dict = ref initdict value
127 val dict = ref thmdict value
[all...] |
| /seL4-l4v-10.1.1/HOL4/src/new-datatype/ |
| H A D | NDatatype.sml | 244 val dict = (vnames, rtcs) value
361 val dict = (ty_names, ty_vars) value
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/ARM/v4/mlton/ |
| H A D | evalML.sml | 276 let val dict = Redblackmap.mkDict String.compare in value
[all...] |
| /seL4-l4v-10.1.1/HOL4/src/parse/ |
| H A D | type_grammar.sml | 235 val (dict, st) = Binarymap.remove(parse_map g, knm) value
|
| H A D | parse_term.sml | 91 let val dict = !r in value
195 type dict = ((stack_terminal * bool) * stack_terminal, type
[all...] |
| /seL4-l4v-10.1.1/HOL4/tools/mllex/ |
| H A D | mllex.sml | 353 structure dict = structure
|