| /seL4-l4v-10.1.1/HOL4/Manual/Interaction/ |
| H A D | HOL-interaction.tex | 258 val TREE_11 = fetch "-" "TREE_11";
259 val TREE_distinct = fetch "-" "TREE_distinct";
|
| /seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Description/ |
| H A D | definitions.tex | 1125 - DB.fetch "-" "fact_ind";
1407 Il teorema d'induzione custom per una funzione si pu� ottenere usando \holtxt{fetch},
1408 che restituisce elementi nominati nella teoria specifica\footnote{In una chiamata a \texttt{fetch}, il
1412 - fetch "-" "qsort_ind";
|
| /seL4-l4v-10.1.1/HOL4/examples/ARM/arm6-verification/ |
| H A D | coreScript.sml | 980 pipebabt`; (* abort on fetch *)
|
| /seL4-l4v-10.1.1/HOL4/examples/ARM/experimental/ |
| H A D | lpc_progScript.sml | 30 val lpc_el_11 = DB.fetch "-" "lpc_el_11";
31 val lpc_el_distinct = DB.fetch "-" "lpc_el_distinct";
|
| /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/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
|
| H A D | arm_evalScript.sml | 45 | NONE => errorT "couldn't fetch an instruction")
46 | NONE => errorT "couldn't fetch an instruction")
47 | NONE => errorT "couldn't fetch an instruction")
48 | NONE => errorT "couldn't fetch an instruction")`;
57 | NONE => errorT "couldn't fetch an instruction")
58 | NONE => errorT "couldn't fetch an instruction"`;
|
| /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))*)
|
| H A D | ARM_prover_extLib.sml | 149 val thrm = SPEC (List.nth(expr,0)) (DB.fetch (current_theory()) ((Hol_pp.term_to_string (opr)) ^ postfix))
|
| /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/CCS/ |
| H A D | CongruenceScript.sml | 1389 val WGS_strongind = DB.fetch "-" "WGS_strongind";
|
| /seL4-l4v-10.1.1/HOL4/examples/Crypto/AES/ |
| H A D | RoundOpScript.sml | 243 THEN RW_TAC std_ss [fetch "Mult" "mult_tables"]
244 THEN REWRITE_TAC [fetch "Mult" "mult_tables"]
|
| /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/examples/Crypto/TEA/ |
| H A D | teaScript.sml | 95 val Rounds_ind = fetch "-" "Rounds_ind"; (* induction *)
|
| /seL4-l4v-10.1.1/HOL4/examples/HolCheck/ |
| H A D | ksTools.sml | 398 (((REWRITE_CONV [ks_def,DB.fetch "ks" "KS_accfupds",combinTheory.K_DEF])
|
| /seL4-l4v-10.1.1/HOL4/examples/PSL/regexp/ |
| H A D | regexpScript.sml | 151 recInduct (fetch "-" "ALL_SPLITS_ind")
355 THEN RW_TAC list_ss [fetch "-" "regexp_size_def"]
|
| /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 | load_book.sml | 42 fun get_acl2_thm s = load_simp_fn(DB.fetch "imported_acl2" (s ^ "_thm"));
|
| 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/ |
| H A D | fmapExample.sml | 893 val outcome_11 = fetch "-" "outcome_11";
894 val outcome_distinct = fetch "-" "outcome_distinct";
895 val outcome_nchotomy = fetch "-" "outcome_nchotomy";
|
| /seL4-l4v-10.1.1/HOL4/examples/acl2/ml/ |
| 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"]);
1583 [fetch "-" "sexp_11",ACL2_TRUE,
|
| 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/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") >>
|
| /seL4-l4v-10.1.1/HOL4/examples/computability/ |
| H A D | goedelCodeScript.sml | 175 val GDECODE_ind = fetch "-" "GDECODE_ind";
|
| /seL4-l4v-10.1.1/HOL4/examples/decidable_separationLogic/src/ |
| H A D | decidable_separationLogicLibScript.sml | 30 val _ = TypeBase.write [TypeBasePure.put_nchotomy nchotomy_thm (valOf (TypeBase.fetch ``:('a,'b,'c) ds_spatial_formula``))];
|