Searched defs:ind (Results 1 - 17 of 17) sorted by relevance

/seL4-l4v-10.1.1/HOL4/examples/theorem-prover/lisp-runtime/extract/
H A Dlisp_synthesisLib.sml23 val ind = fetch "-" ind_name handle HOL_ERR _ => TRUTH value
H A Dlisp_extractLib.sml40 val ind = (SOME (fetch "-" (name^"_ind") |> PURE_REWRITE_RULE [pairTheory.PAIR_EQ]) value
506 val ind = fetch "-" (good_name ^ "_ind") value
[all...]
/seL4-l4v-10.1.1/HOL4/examples/fun-op-sem/cbv-lc/
H A DoptScript.sml30 val ind = SIMP_RULE (srw_ss()) [FORALL_PROD, wf_lem] (Q.ISPEC `(($< :(num->num->bool)) LEX value
/seL4-l4v-10.1.1/HOL4/src/prekernel/
H A DFinalType-sig.sml31 val ind : hol_type value
/seL4-l4v-10.1.1/HOL4/examples/dev/sw2/
H A Dcompiler.sml231 val ind = Defn.ind_of defn2 value
/seL4-l4v-10.1.1/HOL4/examples/dev/sw2/examples/
H A Darm_compiler_demoScript.sml43 val ind = find_ind_thm def value
/seL4-l4v-10.1.1/HOL4/src/1/
H A DMutual.sml317 val ind = GENL vs (SUBST [bool |-> GALPHA asm] (mk_imp(bool, con)) dis) value
H A DPrim_rec.sml650 val ind = GEN v (SUBST [boolvar |-> GALPHA asm] value
1247 val ind = CONV_RULE value
/seL4-l4v-10.1.1/HOL4/src/0/
H A DType.sml66 val ind = Tyapp ((ind_tyid,0), []); value
/seL4-l4v-10.1.1/HOL4/src/experimental-kernel/
H A DType.sml85 val ind = mk_type("ind", []) value
/seL4-l4v-10.1.1/HOL4/src/TeX/
H A DmungeTools.sml465 val (ind,iact) = optset_indent opts value
510 val (ind,iact) = optset_indent opts value
526 val (ind, iact) = optset_indent opts value
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/
H A Dselftest.sml623 val ind = 6 value
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/
H A Dselftest.sml623 val ind = 6 value
/seL4-l4v-10.1.1/HOL4/examples/theorem-prover/milawa-prover/
H A Dmilawa_execScript.sml2131 val ind = value
/seL4-l4v-10.1.1/HOL4/src/real/
H A DRealArith.sml89 fun ind n [] = failwith "index" function
96 fun ind n [] = failwith "index_ac" function
/seL4-l4v-10.1.1/HOL4/src/tfl/src/
H A DDefn.sml970 val ind = Induction.mk_induction theory value
1156 val ind = TypeBasePure.induction_of tyinfo value
1201 val ind = Induction.mk_induction facts value
1903 val ind = CONJUNCT2 th value
[all...]
/seL4-l4v-10.1.1/HOL4/examples/acl2/ml/
H A DpolytypicLib.sml3414 val ind = get_source_ind get_func t value
3427 val ind = get_source_ind get_func t value

Completed in 202 milliseconds