| /seL4-l4v-10.1.1/HOL4/examples/machine-code/graph/ |
| H A D | graph_specsLib.sml | 450 val thms = derive_specs_for sec_name value
|
| H A D | derive_specsLib.sml | 640 val thms = map (triple_apply foo) thms value
681 val thms = snd (derive_individual_specs code) value
687 val thms = try_map (fn (n,_,_) => add_stack_intro_fail n sec_name) value
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/arm/ |
| H A D | prog_armLib.sml | 531 val thms = [arm_step "v6" s] value
532 val thms = (thms @ [arm_step "v6,fail" s]) handle HOL_ERR _ => thms value
533 val thms = map (RW [minus_one,minus_one_mult]) thms value
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/HolCheck/ |
| H A D | cacheTools.sml | 72 val thms = List.map (fn g => let (*val _ = dbgTools.DTM (dpfx^ g) val _ = dbgTools.DST (dpfx^ " goal\n") (*DBG*)*) value
|
| /seL4-l4v-10.1.1/HOL4/examples/acl2/ml/ |
| H A D | acl2encodeLib.sml | 817 val thms = map (FULL_DECODE_ENCODE_THM sexp) types value
|
| H A D | encodeLib.sml | 1609 val thms = map (generate_coding_theorem target "encode_decode_map") rts value
1641 val thms value
1657 val thms = map (generate_source_theorem "map_compose") rts value
1672 val thms = map (generate_coding_theorem target "encode_detect_all") (relevant_types t) value
1744 val thms = map (generate_coding_theorem target "decode_encode_fix" o base_type) rts @ value
1779 val thms = map (fn a => (C (PART_MATCH I) (snd (strip_forall (mk_fix_id_conc target a))) o FULL_FIX_ID_THM target) a) ftypes; value
1800 val thms = mapfilter (GEN_ALL o (CONV_RULE (DEPTH_CONV RIGHT_IMP_FORALL_CONV THENC value
1860 val thms = [K_THM,get_coding_function_def target (mk_prod(alpha,beta)) "decode",I_THM]; value
[all...] |
| H A D | extendTranslateScript.sml | 438 val thms = [DIVISION,ADD_0,MOD_GCD,MULT_EQ_0,GCD_SYM, value
|
| H A D | signedintScript.sml | 442 val thms = [BIT_MOD,DECIDE ``b - 1 < b = 0n < b``,int_sub_calc1,INT_EXP, value
|
| /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/arm/prog/ |
| H A D | arm_progLib.sml | 807 val thms = step s value
|
| /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/m0/prog/ |
| H A D | m0_progLib.sml | 605 val thms = step s value
606 val thms = case (thms, stm_base s) of value
|
| /seL4-l4v-10.1.1/HOL4/src/basicProof/ |
| H A D | BasicProvers.sml | 496 else let val thms = map ASSUME new value
|
| /seL4-l4v-10.1.1/HOL4/src/emit/ |
| H A D | basis_emitScript.sml | 39 let val thms = List.take(CONJUNCTS(SPEC_ALL numeral_add), 6) value
|
| /seL4-l4v-10.1.1/HOL4/src/list/src/ |
| H A D | ListConv1.sml | 241 val thms = map (INST_TYPE [alpha_ty |-> ty]) [leq,lne,nel] value
|
| /seL4-l4v-10.1.1/HOL4/src/n-bit/ |
| H A D | blastLib.sml | 1140 val thms = Lib.mapfilter BIT_BLAST_CONV tms value
|
| /seL4-l4v-10.1.1/HOL4/src/tfl/src/ |
| H A D | Induction.sml | |
| H A D | RW.sml | [all...] |
| /seL4-l4v-10.1.1/HOL4/examples/theorem-prover/lisp-runtime/extract/ |
| H A D | lisp_extractLib.sml | 467 val thms = map derive_thm data value
940 val thms = map prove_corr ps value
|
| /seL4-l4v-10.1.1/HOL4/examples/theorem-prover/lisp-runtime/implementation/ |
| H A D | lisp_codegenScript.sml | 1600 val thms = map simple_spec code value
|
| H A D | lisp_compiler_opScript.sml | 16 val thms = DB.match [] ``SPEC X64_MODEL`` value
17 val thms = filter (can (find_term (can (match_term ``zLISP``))) o car o concl) (map (fst o snd) thms) value
18 val thms = map (Q.INST [`ddd`|->`SOME F`,`cu`|->`NONE`]) thms value
4180 val thms = DB.match [] ``SPEC X64_MODEL`` value
4181 val thms = filter (can (find_term (can (match_term ``zLISP``))) o car o concl) (map (fst o snd) thms) value
4182 val thms value
4265 val thms = [SPEC_COMPOSE_RULE [X64_LISP_ERROR_11,X64_LISP_SET_OK_F]] value
4266 val thms = map (RW [GSYM no_such_function_bool_def]) thms value
4267 val thms = map (Q.INST [`ddd`|->`SOME T`,`cu`|->`NONE`]) thms value
4605 val thms = DB.match [] ``SPEC X64_MODEL`` value
4606 val thms = filter (can (find_term (can (match_term ``zLISP``))) o car o concl) (map (fst o snd) thms) value
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/common/ |
| H A D | utilsLib.sml | 355 val thms = Drule.CONJUNCTS (Q.SPEC `t` boolTheory.IMP_CLAUSES) value
790 val thms = value
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/mips/step/ |
| H A D | mips_stepLib.sml | 104 val thms = ref ([]: thm list) value
1163 val thms = List.map (fn f => STATE_CONV (f tm)) value
[all...] |
| /seL4-l4v-10.1.1/HOL4/src/finite_map/ |
| H A D | finite_mapScript.sml | 113 let val thms = CONJUNCTS fmap_ISO_DEF value
|
| /seL4-l4v-10.1.1/HOL4/src/floating-point/ |
| H A D | binary_ieeeScript.sml | 1522 val thms = value
|
| /seL4-l4v-10.1.1/HOL4/src/quotient/examples/ |
| H A D | ind_rel.sml | 1029 val thms = CONJUNCTS (SPEC_ALL AND_CLAUSES) value
|
| /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/m0/step/ |
| H A D | m0_stepLib.sml | 590 val thms = ref wbit_thms value
[all...] |