/seL4-l4v-10.1.1/HOL4/src/patricia/ |
H A D | sptreeLib.sml | 89 (Option.valOf (TypeBase.fetch ``:'a sptree$spt``))
|
/seL4-l4v-10.1.1/HOL4/src/sort/ |
H A D | mergesortScript.sml | 68 val merge_ind = fetch "-" "merge_ind"; 90 val mergesortN_ind = fetch "-" "mergesortN_ind"; 133 val merge_tail_ind = fetch "-" "merge_tail_ind"; 159 val mergesortN_tail_ind = fetch "-" "mergesortN_tail_ind";
|
/seL4-l4v-10.1.1/HOL4/examples/dev/Fact32/ |
H A D | Fact32Script.sml | 50 val MultIter_ind = fetch "-" "MultIter_ind"; 93 val Mult32Iter_ind = fetch "-" "Mult32Iter_ind"; 211 val FactIter_ind = fetch "-" "FactIter_ind";
|
/seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/deep_embeddings/ |
H A D | kripke_structureScript.sml | 46 val kripke_structure_S = DB.fetch "-" "kripke_structure_S"; 47 val kripke_structure_P = DB.fetch "-" "kripke_structure_P"; 48 val kripke_structure_S0 = DB.fetch "-" "kripke_structure_S0"; 49 val kripke_structure_R = DB.fetch "-" "kripke_structure_R"; 50 val kripke_structure_L = DB.fetch "-" "kripke_structure_L"; 51 val kripke_structure_11 = DB.fetch "-" "kripke_structure_11";
|
H A D | alternating_omega_automataScript.sml | 76 val alternating_semi_automaton_S = DB.fetch "-" "alternating_semi_automaton_S"; 77 val alternating_semi_automaton_I = DB.fetch "-" "alternating_semi_automaton_I"; 78 val alternating_semi_automaton_S0 = DB.fetch "-" "alternating_semi_automaton_S0"; 79 val alternating_semi_automaton_R = DB.fetch "-" "alternating_semi_automaton_R"; 80 val alternating_automaton_A = DB.fetch "-" "alternating_automaton_A"; 81 val alternating_automaton_AC = DB.fetch "-" "alternating_automaton_AC"; 83 val alternating_run_S0 = DB.fetch "-" "alternating_run_S0"; 84 val alternating_run_R = DB.fetch "-" "alternating_run_R";
|
/seL4-l4v-10.1.1/HOL4/examples/hardware/port/tamarack2/ |
H A D | tamarackProof1Script.sml | 25 fun definition x y = SPEC_ALL (DB.fetch x y); 53 val LESS_MOD_THM = DB.fetch "arithmetic" "LESS_MOD"; 55 val MOD_LESS_THM = DB.fetch "arithmetic" "MOD_LESS";
|
H A D | tamarackProof2Script.sml | 25 fun definition x y = SPEC_ALL (DB.fetch x y); 26 fun theorem x y = DB.fetch x y;
|
/seL4-l4v-10.1.1/HOL4/src/tactictoe/src/ |
H A D | tttRecord.sml | 203 String.concatWith " " ["(","DB.fetch",mlquote cthy,mlquote name,")"] 223 ["(","DB.fetch",mlquote thy,mlquote name,")"]) 245 val fetch = total_time fetch_thm_time fetch_thm value
|
H A D | tttPredict.sml | 136 can (DB.fetch a) b 202 a = namespace_tag orelse uptodate_thm (DB.fetch a b)
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/cheri/step/ |
H A D | cheri_stepLib.sml | 40 fun fetch v = function 42 val fetch_hex = fetch o bitstringSyntax.bitstring_of_hexstring 330 val thms = List.map (DB.fetch "cheri_step") cheri_stepTheory.rwts 407 val thm1 = fetch v
|
/seL4-l4v-10.1.1/HOL4/src/floating-point/ |
H A D | machine_ieeeScript.sml | 108 (Rewrite.PURE_REWRITE_CONV [DB.fetch "machine_ieee" ("fp64_" ^ s)])
|
/seL4-l4v-10.1.1/HOL4/examples/ARM/v7/ |
H A D | armScript.sml | 4 (* Top-level: fetch and run instructions *)
|
/seL4-l4v-10.1.1/HOL4/examples/ARM_security_properties/model/ |
H A D | armScript.sml | 4 (* Top-level: fetch and run instructions *)
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/common/ |
H A D | utilsLib.sml | 616 val component_equality = DB.fetch Thy (Tyop ^ "_component_equality") 1035 computeLib.add_datatype_info cmp o Option.valOf o TypeBase.fetch 1074 List.map (fn t => DB.fetch thy t) (l @ m) @ thms 1127 val f = DB.fetch thy 1162 val ftch = DB.fetch thy 1227 val tac = SIMP_TAC (srw_ss()) [DB.fetch thy "Run_def"] 1237 val tac = SIMP_TAC (srw_ss()) [DB.fetch thy "Run_def"] 1251 val tac = SIMP_TAC (srw_ss()) [DB.fetch thy "Run_def"]
|
/seL4-l4v-10.1.1/HOL4/src/Boolify/src/ |
H A D | Encode.sml | 204 [CONJUNCT1 (DB.fetch "list" "APPEND"), DB.fetch "list" "APPEND_NIL"]
|
/seL4-l4v-10.1.1/HOL4/src/integer/testing/ |
H A D | test_cases.sml | 40 fun A s = ("at."^s, concl (DB.fetch "arithmetic" s), true) 41 fun I s = ("it."^s, concl (DB.fetch "integer" s), true)
|
/seL4-l4v-10.1.1/HOL4/examples/ARM/v7/eval/ |
H A D | arm_emitScript.sml | 83 (fetch "arm_opsem" "data_processing_instr") 104 val l = map (fetch "arm_opsem") arm_opsemTheory.instruction_list
|
/seL4-l4v-10.1.1/HOL4/examples/acl2/ml/ |
H A D | tutorial.ml | 52 val propagation_exp = fetch "-" "prop_exp"; 70 val propagation_length = fetch "-" "prop_length"; 92 val translated_listnum = fetch "-" "translated_listnum"; 94 val propagation_listnum = fetch "-" "prop_listnum"; 116 val propagation_natp_list = fetch "-" "natp_list"; 531 val prop_reverse = fetch "-" "prop_reverse"; 783 val propagate_wordp = fetch "-" "prop_wordp"; 860 list_def,atom_def,not_def,GSYM (fetch "-" "prop_numarraylistp"),
|
/seL4-l4v-10.1.1/HOL4/examples/theorem-prover/milawa-prover/ |
H A D | milawa_logicScript.sml | 62 val logic_term_size_def = fetch "-" "logic_term_size_def"; 963 HO_MATCH_MP_TAC (fetch "-" "EvalTerm_ind") 1073 HO_MATCH_MP_TAC (fetch "-" "EvalTerm_ind") 1279 HO_MATCH_MP_TAC (fetch "-" "EvalTerm_ind") \\ SIMP_TAC std_ss [] 1309 HO_MATCH_MP_TAC (fetch "-" "term_ok_ind") \\ SIMP_TAC std_ss [term_ok_def] 1327 HO_MATCH_MP_TAC (fetch "-" "term_ok_ind") 1360 fetch "-" "func_body_distinct",pairTheory.PAIR_EQ]) 1407 \\ METIS_TAC [fetch "-" "func_body_distinct",pairTheory.PAIR_EQ, 1699 HO_MATCH_MP_TAC (fetch "-" "callmap_ind") \\ REVERSE (REPEAT STRIP_TAC) 1806 HO_MATCH_MP_TAC (fetch " [all...] |
H A D | milawa_initScript.sml | 226 \\ ONCE_REWRITE_TAC [fetch "-" "define_safe_list_side_def"] 227 \\ ASM_SIMP_TAC std_ss [LET_DEF,fetch "-" "define_safe_side_def", 233 SIMP_TAC std_ss [fetch "-" "milawa_init_side_def",
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/examples/ |
H A D | simple_examples.sml | 122 HO_MATCH_MP_TAC (fetch "-" "fact_ind") THEN
|
/seL4-l4v-10.1.1/HOL4/examples/fun-op-sem/cbv-lc/ |
H A D | typesScript.sml | 33 val type_size_def = fetch "-" "type_size_def";
|
/seL4-l4v-10.1.1/HOL4/examples/fun-op-sem/small-step/ |
H A D | simple_traceScript.sml | 50 val check_trace_ind = fetch "-" "check_trace_ind";
|
/seL4-l4v-10.1.1/HOL4/src/1/ |
H A D | TypeBasePure.sig | 100 val fetch : typeBase -> hol_type -> tyinfo option value
|
/seL4-l4v-10.1.1/HOL4/examples/theorem-prover/lisp-runtime/spec/ |
H A D | lisp_semanticsScript.sml | 33 val term_11 = fetch "-" "term_11"; 34 val term_distinct = fetch "-" "term_distinct"; 35 val term_size_def = fetch "-" "term_size_def"; 36 val func_11 = fetch "-" "func_11";
|