| /seL4-l4v-master/HOL4/src/postkernel/ |
| H A D | HolKernel.sml | 747 val insts = term_homatch tyavoids lconsts tyins pinsts_homs value
[all...] |
| /seL4-l4v-master/HOL4/examples/machine-code/graph/ |
| H A D | graph_specsLib.sml | 515 val insts = try_map (fn (_,(th,_,_),_) => value
545 val insts = map remove_SKIP_TAG insts value
|
| /seL4-l4v-master/graph-refine/ |
| H A D | trace_refute.py | 635 insts = [arg for arg in args if arg.startswith ('instance:')] variable
|
| /seL4-l4v-master/HOL4/src/TeX/ |
| H A D | mungeTools.sml | 259 val insts = List.mapPartial (fn Inst(s1,s2) => SOME (s1,s2) | _ => NONE) value
313 val (insts, tytheta, theta) = mkinst loc opts (concl th) value
322 val (insts, tytheta, theta) = mkinst loc opts tm value
[all...] |
| /seL4-l4v-master/HOL4/src/taut/ |
| H A D | tautLib.sml | 188 val insts = HOLset.listItems (non_prop_terms tm') value
|
| /seL4-l4v-master/HOL4/src/num/arith/src/ |
| H A D | Instance.sml | 75 val insts = Lib.op_mk_set aconv (detector tm') value
|
| /seL4-l4v-master/HOL4/src/n-bit/ |
| H A D | blastLib.sml | 907 val insts = HOLset.listItems (non_prop_terms tm) value
972 val insts = HOLset.listItems (non_prop_terms tm) value
|
| /seL4-l4v-master/HOL4/src/emit/ |
| H A D | ConstMapML.sml | 76 val insts = Listsort.sort icmp insts0 value
|
| /seL4-l4v-master/HOL4/src/IndDef/ |
| H A D | InductiveDefinition.sml | 619 val insts = map2 (curry op |->) (map lhs defs) (map (lhs o concl) dths) value
|
| /seL4-l4v-master/HOL4/src/HolSat/ |
| H A D | dpll.sml | 103 let val insts = RBM.foldl (fn (v,t,insts) => (v |-> t)::insts) [] lfn value
|
| /seL4-l4v-master/HOL4/examples/ |
| H A D | dpll.sml | 152 val insts = HOLset.listItems (var_leaves empty_tmset tm') value
|
| /seL4-l4v-master/HOL4/examples/dev/sw2/ |
| H A D | monomorphisation.sml | 295 val insts = M.listItems(M.find(imap, f_str)) handle _ => [] value
|
| /seL4-l4v-master/HOL4/examples/dev/sw/working/0.2/ |
| H A D | IR.sml | 192 val insts = flow [ Tree.CJUMP(analyzeExp c, t_lab), value
|
| H A D | CFG.sml | 173 val insts = Lib.flatten (List.map (fn inst => one_stm inst) stmList); value
|
| /seL4-l4v-master/HOL4/examples/dev/sw/working/0.1/ |
| H A D | IR.sml | 192 val insts = flow [ Tree.CJUMP(analyzeExp c, t_lab), value
|
| H A D | CFG.sml | 173 val insts = Lib.flatten (List.map (fn inst => one_stm inst) stmList); value
|
| /seL4-l4v-master/HOL4/examples/dev/sw/ |
| H A D | IR.sml | 201 val insts = flow [ Tree.CJUMP(analyzeExp c, t_lab), value
|
| H A D | CFG.sml | 172 val insts = Lib.flatten (List.map (fn inst => one_stm inst) stmList); value
|