Searched defs:thms (Results 1 - 25 of 83) sorted by relevance

1234

/seL4-l4v-10.1.1/HOL4/examples/machine-code/compiler/demo/
H A Dcompiler_demoScript.sml110 val (thms,arm_str_rev_def,arm_str_rev_pre_def) = compile_all `` value
/seL4-l4v-10.1.1/HOL4/src/quotient/src/
H A Dselftest.sml22 val thms = define_equivalence_type { value
31 val thms = define_equivalence_type { value
/seL4-l4v-10.1.1/HOL4/examples/machine-code/lisp/
H A Dlisp_evalScript.sml7 val thms = DB.match [] ``SPEC ARM_MODEL`` value
8 val thms = filter (can (find_term (can (match_term ``aLISP``))) o concl) (map (fst o snd) thms) value
10 val thms = map renamer thms value
16 val thms = DB.match [] ``SPEC PPC_MODEL`` value
17 val thms = filter (can (find_term (can (match_term ``pLISP``))) o concl) (map (fst o snd) thms) value
19 val thms value
25 val thms = DB.match [] ``SPEC X86_MODEL`` value
26 val thms = filter (can (find_term (can (match_term ``xLISP``))) o concl) (map (fst o snd) thms) value
29 val thms = map renamer thms value
41 val (thms,_,_) = compile_all `` value
[all...]
/seL4-l4v-10.1.1/HOL4/src/string/
H A DASCIInumbersLib.sml17 val thms = value
/seL4-l4v-10.1.1/HOL4/src/opentheory/compat/
H A DOpenTheoryBoolScript.sml19 val thms = read_article file reader; value
H A DOpenTheoryFunctionScript.sml19 val thms = read_article file reader; value
H A DOpenTheoryRelationScript.sml40 val thms = read_article file reader; value
/seL4-l4v-10.1.1/HOL4/src/list/src/
H A DnumposrepLib.sml22 val thms = value
/seL4-l4v-10.1.1/HOL4/src/num/extra_theories/
H A DbitLib.sml31 val thms = value
46 val thms = value
/seL4-l4v-10.1.1/HOL4/src/opentheory/postbool/
H A DOpenTheoryIO.sml20 val thms = raw_read_article inp { value
/seL4-l4v-10.1.1/HOL4/src/pred_set/src/
H A Dpred_setLib.sml46 val thms = value
/seL4-l4v-10.1.1/HOL4/src/sort/
H A DternaryComparisonsScript.sml11 val thms = value
/seL4-l4v-10.1.1/HOL4/examples/theorem-prover/lisp-runtime/extract/
H A Dlisp_synthesis_demoScript.sml70 val thms = synthesise_deep_embeddings () value
/seL4-l4v-10.1.1/HOL4/examples/ARM/arm6-verification/correctness/
H A Diclass_compScript.sml72 val thms = save_thm("iclass_comp_thms", value
/seL4-l4v-10.1.1/HOL4/src/1/
H A DDiskThms.sml14 val thms = map #2 named_thms value
H A DRewrite.sml258 val thms = dest_rewrites rws value
[all...]
H A DThmSetData.sml142 val thms = valOf (dest d) value
/seL4-l4v-10.1.1/HOL4/src/num/arith/src/
H A DTheorems.sml85 val thms = CONJUNCTS (SPEC_ALL (arithmeticTheory.MULT_CLAUSES)) value
/seL4-l4v-10.1.1/HOL4/src/postkernel/
H A DDB.sig13 val thms : string -> (string * thm) list value
/seL4-l4v-10.1.1/HOL4/examples/machine-code/graph/
H A Dcond_cleanLib.sml115 val thms = list_append_nop_to_if thms value
[all...]
H A DstraightlineLib.sml106 val thms = map (fn ys => let value
/seL4-l4v-10.1.1/HOL4/src/HolSmt/
H A DLibrary.sml267 val thms = [pred_setTheory.SPECIFICATION, pred_setTheory.GSPEC_ETA, value
/seL4-l4v-10.1.1/HOL4/src/floating-point/
H A Dmachine_ieeeScript.sml12 val thms = (List.concat o List.map machine_ieeeLib.mk_fp_encoding) value
/seL4-l4v-10.1.1/HOL4/src/metis/
H A DmlibMetis.sml187 val {thms,hyps} = clauses goal value
/seL4-l4v-10.1.1/HOL4/src/compute/examples/
H A DMergeSort.sml8 val thms = ref ([] : thm list); value

Completed in 146 milliseconds

1234