Searched refs:fetch (Results 151 - 162 of 162) sorted by relevance

1234567

/seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/
H A DseparationLogicScript.sml4567 val asl_prim_command_11 = fetch "-" "asl_prim_command_11";
4647 val asl_atomic_action_11 = fetch "-" "asl_atomic_action_11";
4648 val asl_atomic_action_distinct = fetch "-" "asl_atomic_action_distinct";
5435 val asl_proto_trace_size_def = fetch "-" "asl_proto_trace_size_def";
5436 val asl_proto_trace_11 = fetch "-" "asl_proto_trace_11";
5437 val asl_proto_trace_distinct = fetch "-" "asl_proto_trace_distinct";
/seL4-l4v-10.1.1/HOL4/examples/formal-languages/regular/
H A Dregexp_compilerScript.sml79 val extend_states_ind = fetch "-" "extend_states_ind";
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/common/
H A DstateLib.sml872 DB.fetch Thy (Name ^ "_def")
/seL4-l4v-10.1.1/HOL4/src/pred_set/src/
H A Dset_relationScript.sml255 (Q.SPECL [`r`, `\(x, y). tc' x y`] (fetch "-" "tc_strongind"))));
H A Dpred_setScript.sml4380 val ITSET_IND = fetch "-" "ITSET_ind";
/seL4-l4v-10.1.1/HOL4/examples/machine-code/garbage-collectors/
H A Dlisp_gcScript.sml1141 val XExp_11 = fetch "-" "XExp_11";
1142 val XExp_distinct = fetch "-" "XExp_distinct";
/seL4-l4v-10.1.1/HOL4/examples/theorem-prover/lisp-runtime/implementation/
H A Dlisp_compiler_opScript.sml766 HO_MATCH_MP_TAC (fetch "-" "SPLIT_LIST_ind")
804 HO_MATCH_MP_TAC (fetch "-" "SPLIT_LIST_ind")
817 HO_MATCH_MP_TAC (fetch "-" "SPLIT_LIST_ind")
H A Dlisp_invScript.sml23 val io_streams_11 = fetch "-" "io_streams_11"
/seL4-l4v-10.1.1/HOL4/examples/theorem-prover/milawa-prover/
H A Dmilawa_proofpScript.sml658 val logic_appeal_size_def = fetch "-" "logic_appeal_size_def"
665 val logic_appeal_size_def = fetch "-" "logic_appeal_size_def"
2495 HO_MATCH_MP_TAC (fetch "-" "a2sexp_ind") \\ REPEAT STRIP_TAC
/seL4-l4v-10.1.1/HOL4/examples/decidable_separationLogic/src/
H A Ddecidable_separationLogicLibScript.sml30 val _ = TypeBase.write [TypeBasePure.put_nchotomy nchotomy_thm (valOf (TypeBase.fetch ``:('a,'b,'c) ds_spatial_formula``))];
/seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/holfoot/
H A DholfootScript.sml44 val holfoot_tag_11 = DB.fetch "-" "holfoot_tag_11";
48 val holfoot_var_11 = DB.fetch "-" "holfoot_var_11";
/seL4-l4v-10.1.1/HOL4/src/pattern_matches/
H A DpatternMatchesLib.sml299 val ti = case TypeBase.fetch ty of

Completed in 285 milliseconds

1234567