/seL4-l4v-master/HOL4/src/parse/ |
H A D | type_grammar.sml | 568 val (inst,{Thy,Name},_) = hd allinsts value
|
H A D | Preterm.sml | 232 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 D | Tactic.sml | 455 val inst = INST_TYPE [Type.alpha |-> type_of larm] COND_CLAUSES value
|
H A D | Drule.sml | 716 val inst = value [all...] |
H A D | TypeBasePure.sml | 630 val inst = Binarymap.foldl (fn (tyk,tyv,acc) => (tyk |-> tyv)::acc) value
|
H A D | Prim_rec.sml | 982 val inst = INST_TYPE [rty |-> B] th value [all...] |
/seL4-l4v-master/graph-refine/ |
H A D | check.py | 398 def inst (exp): function in function:split_hyps_at_visit
|
/seL4-l4v-master/HOL4/src/tfl/src/ |
H A D | Defn.sml | |
/seL4-l4v-master/HOL4/examples/AI_tasks/ |
H A D | mleDiophProve.sml | 238 val inst = (INST [{redex = cP, residue = pdef}, value
|
/seL4-l4v-master/HOL4/src/coretypes/ |
H A D | sumScript.sml | 263 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 D | Term.sml | 610 fun inst [] tm = tm function
|
/seL4-l4v-master/HOL4/src/quotient/src/ |
H A D | quotient.sml | 523 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 D | ind_rel.sml | 878 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 D | FinalTerm-sig.sml | 66 val inst : (hol_type,hol_type) subst -> term -> term value
|
/seL4-l4v-master/HOL4/src/pred_set/src/ |
H A D | PSet_ind.sml | 64 val inst = INST_TYPE [alpha |-> ty] FINITE_INDUCT value
|
H A D | PGspec.sml | 52 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 D | constrFamiliesLib.sml | 76 val inst = Binarymap.foldl (fn (tyk,tyv,acc) => (tyk |-> tyv)::acc) value
|
/seL4-l4v-master/HOL4/src/hol88/ |
H A D | hol88Lib.sml | 31 val inst = Term.inst o subst_of value
|
H A D | hol88Lib.sig | 38 val inst : (hol_type,hol_type)hol88subst -> term -> term value
|
/seL4-l4v-master/HOL4/src/experimental-kernel/ |
H A D | Term.sml | 765 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 D | lisp_codegenScript.sml | 961 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 D | lisp_opsScript.sml | 558 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 D | binderLib.sml | 341 val inst = match_type (type_of to_munge) (type_of src) value
|
/seL4-l4v-master/HOL4/examples/l3-machine-code/riscv/model/ |
H A D | riscv.sml | 14517 val inst = Decode w value
|
/seL4-l4v-master/HOL4/examples/hardware/hol88/tamarack2/ |
H A D | tamarack.ml | 254 let inst = Inst n (mem,pc) in var
|