Searched defs:inst (Results 1 - 25 of 37) sorted by last modified time

12

/seL4-l4v-master/HOL4/src/parse/
H A Dtype_grammar.sml568 val (inst,{Thy,Name},_) = hd allinsts value
H A DPreterm.sml232 val inst = ListPair.map (fn (p,a) => p |-> a) (bvs, args) value
306 val inst = ListPair.map Lib.|-> (bvs, args) value
/seL4-l4v-master/HOL4/src/1/
H A DTactic.sml455 val inst = INST_TYPE [Type.alpha |-> type_of larm] COND_CLAUSES value
H A DDrule.sml716 val inst = value
[all...]
H A DTypeBasePure.sml630 val inst = Binarymap.foldl (fn (tyk,tyv,acc) => (tyk |-> tyv)::acc) value
H A DPrim_rec.sml982 val inst = INST_TYPE [rty |-> B] th value
[all...]
/seL4-l4v-master/graph-refine/
H A Dcheck.py398 def inst (exp): function in function:split_hyps_at_visit
/seL4-l4v-master/HOL4/src/tfl/src/
H A DDefn.sml
/seL4-l4v-master/HOL4/examples/AI_tasks/
H A DmleDiophProve.sml238 val inst = (INST [{redex = cP, residue = pdef}, value
/seL4-l4v-master/HOL4/src/coretypes/
H A DsumScript.sml263 let val inst = INST_TYPE [Type.gamma |-> Type.bool] sum_axiom value
279 let val inst = INST_TYPE [Type.gamma |-> Type.bool] sum_axiom value
295 let val inst = INST_TYPE [Type.gamma |-> Type.alpha] sum_axiom value
311 let val inst = INST_TYPE [Type.gamma |-> Type.beta] sum_axiom value
/seL4-l4v-master/HOL4/src/0/
H A DTerm.sml610 fun inst [] tm = tm function
/seL4-l4v-master/HOL4/src/quotient/src/
H A Dquotient.sml523 val inst = ASSUME (���^cty_REP a = ^rcl���) value
953 val inst = ASSUME (���^cty_REP a = ^rcl���) value
[all...]
/seL4-l4v-master/HOL4/src/quotient/examples/
H A Dind_rel.sml878 val inst = INST (fst(match_term res ant)) (SPECL avs ax) value
961 val inst = fst(match_term (concl th3) pat) value
/seL4-l4v-master/HOL4/src/prekernel/
H A DFinalTerm-sig.sml66 val inst : (hol_type,hol_type) subst -> term -> term value
/seL4-l4v-master/HOL4/src/pred_set/src/
H A DPSet_ind.sml64 val inst = INST_TYPE [alpha |-> ty] FINITE_INDUCT value
H A DPGspec.sml52 val inst = SYM(SPEC v (INST_TYPE [alpha |-> ty1, beta |-> ty2] PAIR)) value
103 let val inst = INST_TYPE [beta |-> bool] value
231 val inst = SPEC v (INST_TYPE [alpha |-> vty, beta |-> uty] GSPEC) value
/seL4-l4v-master/HOL4/src/pattern_matches/
H A DconstrFamiliesLib.sml76 val inst = Binarymap.foldl (fn (tyk,tyv,acc) => (tyk |-> tyv)::acc) value
/seL4-l4v-master/HOL4/src/hol88/
H A Dhol88Lib.sml31 val inst = Term.inst o subst_of value
H A Dhol88Lib.sig38 val inst : (hol_type,hol_type)hol88subst -> term -> term value
/seL4-l4v-master/HOL4/src/experimental-kernel/
H A DTerm.sml765 fun inst [] tm = tm function
769 val inst : (hol_type, hol_type) Lib.subst -> term -> term = inst value
/seL4-l4v-master/HOL4/examples/theorem-prover/lisp-runtime/implementation/
H A Dlisp_codegenScript.sml961 val inst = ``iCONST_NUM (getVal x0)`` value
1040 val inst value
1298 val inst = ``iJUMP (getVal x0)`` value
1307 val inst = ``iCALL (getVal x0)`` value
1316 val inst = ``iJNIL (getVal x0)`` value
1519 val inst = ``iPOPS (getVal x0)`` value
1528 val inst = ``iSTORE (getVal x0)`` value
1537 val inst = ``iLOAD (getVal x0)`` value
1964 val inst = ``iJUMP (getVal x0)`` value
1974 val inst = ``iJNIL (getVal x0)`` value
[all...]
/seL4-l4v-master/HOL4/examples/machine-code/lisp/
H A Dlisp_opsScript.sml558 val inst = "E1A0"^(int_to_string (i+2))^"00"^(int_to_string (j+2)) value
627 val inst = "E59"^(int_to_string (j+2))^(int_to_string (i+2))^"000" value
705 val inst = "E59"^(int_to_string (j+2))^(int_to_string (i+2))^"004" value
1195 val inst = "E13"^(int_to_string (i+2))^"000"^(int_to_string (j+2)) value
/seL4-l4v-master/HOL4/examples/lambda/basics/
H A DbinderLib.sml341 val inst = match_type (type_of to_munge) (type_of src) value
/seL4-l4v-master/HOL4/examples/l3-machine-code/riscv/model/
H A Driscv.sml14517 val inst = Decode w value
/seL4-l4v-master/HOL4/examples/hardware/hol88/tamarack2/
H A Dtamarack.ml254 let inst = Inst n (mem,pc) in var

Completed in 340 milliseconds

12