| /seL4-l4v-10.1.1/HOL4/src/search/ |
| H A D | dftScript.sml | 117 THEN HO_MATCH_MP_TAC (fetch "-" "DFT_ind")
|
| /seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/deep_embeddings/ |
| H A D | symbolic_semi_automatonScript.sml | 86 val symbolic_semi_automaton_S = DB.fetch "-" "symbolic_semi_automaton_S";
87 val symbolic_semi_automaton_S0 = DB.fetch "-" "symbolic_semi_automaton_S0";
88 val symbolic_semi_automaton_R = DB.fetch "-" "symbolic_semi_automaton_R";
89 val symbolic_semi_automaton_11 = DB.fetch "-" "symbolic_semi_automaton_11";
|
| /seL4-l4v-10.1.1/HOL4/examples/Crypto/TEA/ |
| H A D | teaScript.sml | 95 val Rounds_ind = fetch "-" "Rounds_ind"; (* induction *)
|
| /seL4-l4v-10.1.1/HOL4/examples/acl2/examples/M1/ |
| H A D | sexpScript.sml | 676 (fetch "-" "sexp_size_def"
1262 THEN PROVE_TAC[fetch "-" "sexp_11",T_NIL]);
1549 fetch "-" "sexp_size_def"]);
1558 fetch "-" "sexp_size_def"]);
1715 [fetch "-" "sexp_11",ACL2_TRUE,
|
| /seL4-l4v-10.1.1/HOL4/examples/acl2/examples/acl2-hol-ltl-paper-example/ |
| H A D | sexpScript.sml | 676 (fetch "-" "sexp_size_def"
1262 THEN PROVE_TAC[fetch "-" "sexp_11",T_NIL]);
1549 fetch "-" "sexp_size_def"]);
1558 fetch "-" "sexp_size_def"]);
1715 [fetch "-" "sexp_11",ACL2_TRUE,
|
| /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/m0/step/ |
| H A D | m0_stepLib.sml | 1041 utilsLib.specialized "fetch"
1055 then raise ERR "fetch" (utilsLib.long_term_to_string l ^ " " ^ s)
1058 fun fetch e = function
1078 else raise ERR "fetch" "length must be 16 or 32"
1085 val ftch = fetch tms
1939 val ftch = fetch be
|
| /seL4-l4v-10.1.1/HOL4/src/tactictoe/src/ |
| H A D | tttTools.sml | 628 then String.concatWith " " ["DB.fetch",mlquote a,mlquote b]
727 else List.mapPartial tid_of_did (depidl_of_thm (DB.fetch a b))
|
| /seL4-l4v-10.1.1/HOL4/examples/theorem-prover/lisp-runtime/implementation/ |
| H A D | lisp_correctnessScript.sml | 371 val abbrev_code_for_compile_inst_def = fetch "-" "abbrev_code_for_compile_inst_def"
372 val abbrev_code_for_compile_def = fetch "-" "abbrev_code_for_compile_def"
|
| /seL4-l4v-10.1.1/HOL4/examples/theorem-prover/milawa-prover/ |
| H A D | milawa_defsScript.sml | 30 SIMP_TAC std_ss [fetch "-" "not_def"] \\ REPEAT STRIP_TAC
34 fetch "-" "R_ev_rank"
|
| /seL4-l4v-10.1.1/HOL4/examples/ARM_security_properties/ |
| H A D | ARM_proverLib.sml | 242 (* (DB.fetch (current_theory()) ((Hol_pp.term_to_string (opr)) ^ ext)) *)
245 (* (DB.fetch (current_theory()) ((Hol_pp.term_to_string (opr)) ^ "_comb"^ ext))*)
|
| /seL4-l4v-10.1.1/HOL4/examples/dev/sw2/ |
| H A D | monomorphisation.sml | 148 let val original_t = (TypeBasePure.ty_of o valOf o TypeBase.fetch) t
|
| /seL4-l4v-10.1.1/HOL4/examples/dev/sw2/test/ |
| H A D | tea.sml | 69 val Rounds_ind = fetch "-" "Rounds_ind";
|
| /seL4-l4v-10.1.1/HOL4/examples/formal-languages/regular/regular-play/src/ |
| H A D | regexMarkedScript.sml | 18 val MReg_rws = type_rws ``:'a MReg``; (*fetch "-" "MReg_distinct"*)
|
| /seL4-l4v-10.1.1/HOL4/examples/fun-op-sem/small-step/ |
| H A D | oracleSemScript.sml | 309 >- metis_tac [fetch "-" "fbs_res_distinct"]
|
| /seL4-l4v-10.1.1/HOL4/src/1/ |
| H A D | TypeBasePure.sml | 689 fun fetch tbase ty = function
786 Option.composePartial (size_of,fetch db)
797 Option.map fst o Option.composePartial (encode_of, fetch db)
896 val Gamma = Option.composePartial (lift_of, fetch db)
|
| /seL4-l4v-10.1.1/HOL4/src/compute/src/ |
| H A D | computeLib.sml | 312 fun add_datatype cmp = add_datatype_info cmp o Option.valOf o TypeBase.fetch
|
| /seL4-l4v-10.1.1/HOL4/src/enumfset/ |
| H A D | comparisonScript.sml | 254 ho_match_mp_tac (fetch "-" "option_cmp2_ind") >>
|
| /seL4-l4v-10.1.1/HOL4/src/num/extra_theories/ |
| H A D | gcdScript.sml | 73 val gcd_ind = GEN_ALL (DB.fetch "-" "gcd_ind");
|
| /seL4-l4v-10.1.1/graph-refine/ |
| H A D | debug.py | 542 def fetch ((n, vc)): function in function:trace_var
559 val2 = fetch ((n, vc))
|
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/garbage-collectors/ |
| H A D | cheney_gcScript.sml | 42 val heap_type_distinct = fetch "-" "heap_type_distinct"
43 val heap_type_11 = fetch "-" "heap_type_11"
142 val cheney_ind = fetch "-" "cheney_ind";
185 \\ METIS_TAC [DECIDE ``n <= k \/ k < n:num``,fetch "-" "heap_type_distinct"]);
|
| H A D | improved_gcScript.sml | 19 val heap_address_11 = fetch "-" "heap_address_11";
20 val heap_address_distinct = fetch "-" "heap_address_distinct";
333 val heap_element_distinct = fetch "-" "heap_element_distinct";
334 val heap_element_11 = fetch "-" "heap_element_11";
|
| /seL4-l4v-10.1.1/HOL4/examples/Crypto/RC6/ |
| H A D | RC6Script.sml | 196 val Round_ind = fetch "-" "Round_ind";
|
| /seL4-l4v-10.1.1/HOL4/help/src-sml/ |
| H A D | ParseDoc.sml | 38 fun fetch str = Substring.string (fetch_contents str); function
|
| /seL4-l4v-10.1.1/HOL4/src/HolSmt/ |
| H A D | Yices.sml | 264 (case TypeBase.fetch ty of
514 case TypeBase.fetch data_ty of
555 case TypeBase.fetch data_ty of
|
| /seL4-l4v-10.1.1/HOL4/examples/balanced_bst/ |
| H A D | balanced_mapScript.sml | 640 val balanceL_ind = fetch "-" "balanceL_ind";
641 val balanceR_ind = fetch "-" "balanceR_ind";
1460 ho_match_mp_tac (fetch "-" "deleteFindMin_ind") >>
1589 ho_match_mp_tac (fetch "-" "deleteFindMax_ind") >>
1973 ho_match_mp_tac (fetch "-" "link_ind") >>
2311 ho_match_mp_tac (fetch "-" "hedgeUnion_ind") >>
3010 ho_match_mp_tac (fetch "-" "submap'_ind") >>
|