| /seL4-l4v-master/HOL4/tools/mlyacc/src/ |
| H A D | absyn-sig.sml | 31 and pat = PVAR of string type
|
| H A D | absyn.sml | 36 and pat type
[all...] |
| /seL4-l4v-master/HOL4/examples/dev/sw/working/0.2/ |
| H A D | simplifier.sml | 10 val pat = lhs(snd(dest_imp(concl thm))) value
|
| H A D | ARMCompositionScript.sml | 37 val pat = lhs(snd(dest_imp(concl thm))) value
|
| /seL4-l4v-master/HOL4/examples/machine-code/graph/ |
| H A D | stack_introLib.sml | 12 val pat = case !arch_name of ARM => ``arm_MEMORY d m`` value
|
| H A D | cond_cleanLib.sml | 10 val pat = ``IMPL_INST code locs (Inst ^loc assert next)`` value
|
| H A D | func_decompileLib.sml | 23 val pat = th |> UNDISCH |> concl |> dest_eq |> fst value
178 val pat = ``locs (name:string) = SOME ^w_var`` value
|
| H A D | exportLib.sml | 65 val pat = ``GraphFunction inps outps gg ep`` value
77 val pat = ``Basic n xs`` value
91 val pat = ``Cond n1 n2 p`` value
102 val pat = ``Call next name args strs`` value
119 val pat = ``NextNode n`` value
128 val pat = ``var_acc str`` value
136 val pat = ``SKIP_TAG str`` value
[all...] |
| /seL4-l4v-master/HOL4/examples/l3-machine-code/common/ |
| H A D | tripleLib.sml | 96 val pat value
[all...] |
| /seL4-l4v-master/HOL4/src/tfl/src/ |
| H A D | Rules.sml | 111 val pat = rhs veq value
|
| /seL4-l4v-master/HOL4/src/integer/ |
| H A D | jrhUtils.sml | 90 val pat = subst[l |-> gv] w value
|
| /seL4-l4v-master/HOL4/examples/bootstrap/ |
| H A D | source_propertiesScript.sml | 315 val pat = hd pats |> fst value
|
| /seL4-l4v-master/HOL4/src/meson/src/ |
| H A D | jrhTactics.sml | 127 val pat = ASSUME (Term.subst [x |-> t] bod) value
|
| /seL4-l4v-master/HOL4/src/metis/ |
| H A D | mlibTermnet.sml | 203 fun pat sub v = case M.peek (sub,v) of NONE => VAR | SOME qtm => qtm; function
231 fun pat NONE = VAR | pat (SOME qtm) = qtm; function
|
| /seL4-l4v-master/HOL4/src/quantHeuristics/ |
| H A D | quantHeuristicsLibAbbrev.sml | 207 val pat = Parse.parse_in_context fvs q value
224 val pat = Parse.parse_in_context fvs q value
|
| /seL4-l4v-master/HOL4/examples/machine-code/acl2/ |
| H A D | m1_progLib.sml | 29 val pat = find_term (can (match_term ``tL a v``)) (concl th) value
|
| /seL4-l4v-master/HOL4/examples/miller/ho_prover/ |
| H A D | ho_basicTools.sml | 233 val pat = LHS th' value
264 val pat = (lhs o snd o dest_imp o concl) th' value
|
| /seL4-l4v-master/HOL4/examples/dev/sw/ |
| H A D | ARMCompositionScript.sml | 23 val pat = lhs(snd(dest_imp(concl thm))) value
|
| /seL4-l4v-master/HOL4/examples/dev/sw/working/0.1/ |
| H A D | ARMCompositionScript.sml | 23 val pat = lhs(snd(dest_imp(concl thm))) value
|
| /seL4-l4v-master/HOL4/src/1/ |
| H A D | Ho_Rewrite.sml | 231 val pat = Lib.trye hd (look_fn stm) value
|
| /seL4-l4v-master/HOL4/src/pattern_matches/ |
| H A D | parsePMATCH.sml | 200 val (pat, guard_opt) = value
|
| /seL4-l4v-master/seL4/src/arch/x86/32/kernel/ |
| H A D | vspace_32paging.c | 39 pde_pde_large_new_phys(uint32_t page_base_address, uint32_t pat, uint32_t avl, uint32_t global, uint32_t dirty, uint32_t accessed, uint32_t cache_disabled, uint32_t write_through, uint32_t super_user, uint32_t read_write, uint32_t present) argument
|
| /seL4-l4v-master/HOL4/examples/elliptic/ |
| H A D | subtypeTools.sml | 69 val pat = lhs eq value
|
| /seL4-l4v-master/HOL4/src/pred_set/src/ |
| H A D | PFset_conv.sml | 173 val pat = mk_eq(lhs(concl thm),mk_cond(bv,v,mk_comb(rator S,v))) value
216 val pat = mk_eq(lhs,mk_cond(bv,v,mk_comb(ins,v))) value
|
| /seL4-l4v-master/HOL4/src/postkernel/ |
| H A D | DB.sml | 227 val pat = toLower pat and s = toLower s value
[all...] |