/seL4-l4v-10.1.1/HOL4/src/postkernel/ |
H A D | HolKernel.sml | 4 open Feedback Globals Lib Type Term Thm Theory 210 val mk_aty = list_mk_rbinop (Lib.curry Type.-->) 219 Term.list_mk_comb (Term.inst (Type.match_type tyl tyr) tm, xs) 504 val name = fst (dest_var (genvar Type.alpha)) 620 if existing = residue then E else failwith "Type bindings clash"
|
H A D | TheoryPP.sml | 12 type hol_type = Type.hol_type 48 let open Portable Type PP 274 add_string "open Type Term Thm" >> add_newline >>
|
H A D | Theory.sig | 4 type hol_type = Type.hol_type
|
/seL4-l4v-10.1.1/HOL4/src/quotient/src/ |
H A D | quotient.sig | 49 val list_cache : unit -> (Type.hol_type * Thm.thm) list 102 Type.hol_type -> (* type, whose equivalence relation is equality *) 141 Type.hol_type -> (* type, whose equivalence relation is desired *) 157 Type.hol_type -> (* type, whose equivalence relation is equality *) 210 Type.hol_type -> (* type (not lifted) of desired quotient *)
|
/seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/ |
H A D | vars_as_resourceBaseFunctor.sml | 829 val base_t0 = inst [Type.alpha |-> var_ty, 830 Type.beta |-> data_ty, 831 Type.gamma |-> (optionSyntax.mk_option data_ty)] var_res_exp_varlist_update_term; 833 val var_exp_t = inst [Type.beta |-> var_ty, Type.alpha |-> data_ty]
|
/seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/holfoot/ |
H A D | holfootParser.sml | 150 val eL_v = genvar (Type `:num list`); 423 (map string2holfoot_tag argL), Type `:holfoot_tag`); 620 val rp_term = pred_setSyntax.prim_mk_set (rL, Type `:holfoot_var`); 621 val wp_term = pred_setSyntax.prim_mk_set (wL, Type `:holfoot_var`); 649 val rp_term = listSyntax.mk_list (var_list, Type `:holfoot_var`); 694 val unit_var_term = mk_var("uv", Type `:unit`); 1110 val arg_ref_term = mk_new_var ("arg_refL", Type `:holfoot_var list`); 1111 val arg_val_term = mk_new_var ("arg_valL", Type `:num list`); 1309 val varL = listSyntax.mk_list (vars, Type `:holfoot_var`); 1314 Type ` [all...] |
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/common/ |
H A D | stateLib.sml | 11 val (Type, Term) = value 94 val ty_name = #Tyop o Type.dest_thy_type o Term.type_of 107 val state_ty = fst (Type.dom_rng ty) 108 val {Thy = thy, ...} = Type.dest_thy_type state_ty 119 (combinSyntax.mk_K_1 (c, Type.alpha), Type.alpha, true) 247 (pairSyntax.mk_prod (Type.dom_rng ty) --> Type.bool) --> Type.bool 326 case Type [all...] |
/seL4-l4v-10.1.1/HOL4/examples/ARM_security_properties/ |
H A D | user_lemma_instructionsScript.sml | 439 val _ = e(ASSUME_TAC (SPECL [``n:word4``, load_multiple_part, ``(assert_mode 16w)``, ``priv_mode_constraints``, ``priv_mode_similar``] (INST_TYPE [alpha |-> Type `:unit`] cpsr_par_simp_rel_lem))); 585 val data_processing_core_part_thm2 = SIMP_RULE (srw_ss()) [(SPECL [data_processing_core_part, ``(assert_mode 16w):(arm_state->bool)``, ``(assert_mode 16w):(arm_state->bool)``] (INST_TYPE [alpha |-> (Type `:(word32 # (word32 # bool) # bool # bool #bool # bool)`), beta |-> type_of (``()``)] second_abs_lemma))] data_processing_core_part_thm1; 595 val _ = e(ASSUME_TAC (SPECL [data_processing_pre_part, data_processing_core_part,``16w:word5``, ``priv_mode_constraints``, ``priv_mode_similar``] (INST_TYPE [alpha |-> Type `:(word32 # (word32 # bool) # bool # bool #bool # bool)`, beta |-> type_of (``()``)] seqT_preserves_relation_uu_thm))); 763 THEN ASSUME_TAC (SPEC ``(��info. if version_number info.arch < 5 then take_undef_instr_exception <|proc := 0|> else take_prefetch_abort_exception <|proc := 0|>)`` (INST_TYPE [alpha |-> Type `:ARMinfo`, beta |-> Type `:unit`] second_abs_lemma)) 765 THEN ASSUME_TAC (SPECL [``(read_info <|proc:=0|>):(ARMinfo M)``, ``( \info. (if version_number info.arch < 5 then take_undef_instr_exception <|proc := 0|> else take_prefetch_abort_exception <|proc := 0|>))``, ``16w:word5``, ``little_mode_mix``, ``little_mode_mix``, ``priv_mode_constraints_v1``, ``priv_mode_similar``] (INST_TYPE [alpha |-> Type `:ARMinfo`, beta |-> Type `:unit`] seqT_preserves_relation_comb_thm))
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/ |
H A D | IRSyntax.sml | 240 mk_list (List.map (term_of_int o index_of_exp) slist, Type `:num`)]), 244 mk_list (List.map (term_of_int o index_of_exp) dlist, Type `:num`)]), 0) 267 val blk = mk_comb (Term`BLK`, mk_list (l1, Type`:DOPER`));
|
/seL4-l4v-10.1.1/HOL4/src/HolSat/ |
H A D | dimacsTools.sml | 6 open Lib boolLib Globals Parse Term Type Thm Drule Conv Feedback 176 then mk_var(((!prefix) ^ Int.toString n), Type.bool) 177 else mk_neg(mk_var(((!prefix) ^ Int.toString(Int.abs n)), Type.bool));
|
H A D | satTools.sml | 10 open Lib boolLib Globals Parse Term Type Thm Drule Psyntax Conv Feedback
|
/seL4-l4v-10.1.1/HOL4/src/TeX/ |
H A D | holindex.sml | 186 | command2string mungeTools.Type = "Type"; 255 List.map (output_holtex_def mungeTools.Type "\\defineHOLty{" os)
|
/seL4-l4v-10.1.1/HOL4/src/holyhammer/ |
H A D | hhWriter.sml | 177 val less_ty = fn a => (fn b => Type.compare (a,b) = LESS) 389 tyvar_names = ref (dempty Type.compare), 437 tyvar_names = ref (dempty Type.compare),
|
H A D | hhTptp.sml | 103 (* Type unsafe version *)
|
/seL4-l4v-10.1.1/HOL4/examples/HolCheck/ |
H A D | ctlScript.sml | 374 val _ = overload_on ("~", mk_const("~",Type`:bool -> bool`)); 377 val _ = overload_on ("~", mk_const("~",Type`:bool -> bool`)); 378 fun prepOverload s = overload_on (s, mk_const(s,Type`:bool -> bool -> bool`));
|
/seL4-l4v-10.1.1/seL4/manual/parts/ |
H A D | bootup.tex | 92 Field Type & Field Name & Description \\ 131 Field Type & Field Name & Description \\ 182 Field Type & Field Name & Description \\
|
/seL4-l4v-10.1.1/HOL4/examples/dev/AES/tupled/ |
H A D | word8Script.sml | 14 val _ = type_abbrev("word8", Type`:bool#bool#bool#bool#bool#bool#bool#bool`);
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.2/ |
H A D | CFLScript.sml | 48 val _ = type_abbrev("MMEM", Type`:num # OFFSET`); (* memory in ir *) 167 val _ = type_abbrev("CEXP", Type`:MREG # COND # MEXP`); 404 (INST_TYPE [alpha |-> Type `:word32 # (num |-> word32) # (num |-> word32)`] UPLOAD_LEM_2)), 408 (INST_TYPE [alpha |-> Type `:word32 # (num |-> word32) # (num |-> word32)`] UPLOAD_LEM_2)),
|
/seL4-l4v-10.1.1/HOL4/src/0/ |
H A D | Net.sig | 37 is supplied when the item is inserted into the net. Type information,
|
/seL4-l4v-10.1.1/HOL4/src/1/ |
H A D | TypeBasePure.sig | 3 type hol_type = Type.hol_type
|
/seL4-l4v-10.1.1/HOL4/src/Boolify/test/ |
H A D | test.sml | 100 MATCH_MP (INST_TYPE [alpha |-> Type`:num`] decode_list)
|
/seL4-l4v-10.1.1/HOL4/src/experimental-kernel/ |
H A D | Net.sig | 37 is supplied when the item is inserted into the net. Type information,
|
/seL4-l4v-10.1.1/HOL4/src/num/arith/src/ |
H A D | numSimps.sml | 21 val (Type,Term) = parse_from_grammars arithmeticTheory.arithmetic_grammars value 290 orelse (is_eq tm andalso type_of (rhs tm) = Type.bool) then 338 (type_of tm = Type.bool) andalso 452 (ty=Type.bool andalso (is_arith tm orelse tm = F))
|
/seL4-l4v-10.1.1/HOL4/src/opentheory/postbool/ |
H A D | Opentheory.sig | 2 type term = Term.term type hol_type = Type.hol_type type thm = Thm.thm
|
/seL4-l4v-10.1.1/HOL4/src/patricia/ |
H A D | patriciaSyntax.sml | 11 Type.mk_thy_type{Tyop="ptree", Thy="patricia", Args = [pty]};
|