/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/x64/prog/ |
H A D | x64_progLib.sig | 4 val x64_spec_code: string quotation -> Thm.thm list
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/x64/step/ |
H A D | x64_stepLib.sig | 4 val x64_step: Term.term list -> Thm.thm 6 val x64_step_code: string quotation -> Thm.thm list 7 val x64_decode: Term.term list -> Thm.thm 9 val x64_decode_code: string quotation -> Thm.thm list
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/graph/ |
H A D | stack_introLib.sig | 4 val STACK_INTRO_RULE : int list -> Thm.thm -> Thm.thm
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/ppc/ |
H A D | ppc_encodeLib.sig | 5 val ppc_supported_instructions : unit -> string list
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/x86/ |
H A D | x86_encodeLib.sig | 5 val x86_supported_instructions : unit -> string list
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/x86_64/ |
H A D | x64_encodeLib.sig | 5 val x64_supported_instructions : unit -> string list
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/x64_compiler/ |
H A D | x64_compilerLib.sig | 6 val x64_compile : term frag list -> thm * thm * thm
|
/seL4-l4v-10.1.1/HOL4/examples/ARM/v7/ |
H A D | arm_encoderLib.sig | 8 val arm_assemble_from_file : string -> (Arbnum.num * string) list * 11 val arm_assemble_from_string : string -> (Arbnum.num * string) list * 14 val arm_assemble_from_quote : string frag list -> 15 (Arbnum.num * string) list *
|
/seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/holfoot/ |
H A D | holfootLib.sig | 8 val combinator_thmL : thm list 10 val final_decision_procedure : thm list -> term -> thm; 12 val resource_proccall_free_thmL : thm list 13 val inital_prop_rewrite_thmL : thm list 14 val abstrL : separationLogicLib.asl_program_abstraction list 15 val comments_step_convL : (conv->conv) list 16 val quantifier_heuristicsL : quantHeuristicsLib.quant_param list 18 (term list -> int -> (bool * simpLib.ssfrag) -> thm list -> term * term * term * term -> thm list) lis [all...] |
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/m0/step/ |
H A D | m0_stepLib.sig | 4 val thumb_step: bool * bool -> string -> Thm.thm list 5 val thumb_step_code: bool * bool -> string quotation -> Thm.thm list list 6 val thumb_step_hex: bool * bool -> string -> Thm.thm list 7 val thumb_decode: bool -> Term.term -> Thm.thm list 8 val thumb_decode_hex: bool -> string -> Thm.thm list 10 val list_instructions: unit -> (string * Term.term) list
|
/seL4-l4v-10.1.1/HOL4/src/portableML/ |
H A D | HOLPP.sig | 14 type 'a quotation = 'a frag list 24 val block : break_style -> int -> pretty list -> pretty 26 val pr_list : 'a pprinter -> pretty list -> 'a list -> pretty list 27 val tabulateWith : (int -> 'a) -> 'a list -> int -> 'a list
|
H A D | smpp.sig | 5 'a * HOLPP.pretty list -> ('b * ('a * HOLPP.pretty list)) option 21 val mapp : ('a -> ('b,unit) t) -> 'a list -> ('b, unit) t 22 val mmap : ('a -> ('b,'c) t) -> 'a list -> ('b, 'c list) t 23 val pr_list : ('b -> ('a,unit)t) -> ('a,unit) t -> 'b list -> ('a,unit)t 24 val mappr_list : ('b -> ('a,'c)t) -> ('a,unit) t -> 'b list -> ('a,'c list) t 37 ustyle : PPBackEnd.pp_style list -> ('a,unit) t -> ('a,unit) t} 41 val backend_style : PPBackEnd.t -> PPBackEnd.pp_style list [all...] |
/seL4-l4v-10.1.1/HOL4/src/tfl/src/ |
H A D | Rules.sig | 13 val EXISTL : term list -> thm -> thm 16 val EVEN_ORS : thm list -> thm list 17 val DISJ_CASESL : thm -> thm list -> thm 22 val SUBS : thm list -> thm -> thm 23 val simpl_conv : thm list -> term -> thm 24 val simplify : thm list -> thm -> thm
|
/seL4-l4v-10.1.1/HOL4/tools/Holmake/ |
H A D | HM_Core_Cline.sig | 8 dontmakes : string list, 12 includes : string list, 32 val fupd_includes : (string list -> string list) -> (t -> t) 37 val core_option_descriptions : t cline_result GetOpt.opt_descr list 39 val sort_descriptions : 'a GetOpt.opt_descr list -> 'a GetOpt.opt_descr list
|
H A D | Holmake_tools.sig | 9 (* simple list things *) 10 val member : ''a -> ''a list -> bool 11 val set_union : ''a list -> ''a list -> ''a list 12 val delete : ''a -> ''a list -> ''a list 13 val set_diff : ''a list -> ''a list -> ''a list [all...] |
/seL4-l4v-10.1.1/HOL4/examples/ARM_security_properties/ |
H A D | ARM_proverLib.sig | 5 val simp_thms_list : Theory.thm list ref 6 val mode_changing_comp_list : Parse.term list ref 8 : Term.term list -> Term.term -> bool 10 : Theory.term -> Theory.term list * Theory.term 15 : Theory.term -> Theory.term list * Theory.term 25 Term.term list -> Abbrev.thm list -> Abbrev.thm * Abbrev.tactic
|
/seL4-l4v-10.1.1/HOL4/examples/acl2/ml/ |
H A D | encodeLib.sig | 50 val type_vars_avoiding_itself : term -> hol_type -> hol_type list 52 val get_sub_types : hol_type -> hol_type -> hol_type list 83 val encode_decode_map_tactic : hol_type -> hol_type -> term list * term -> 84 (term list * term) list * (thm list -> thm) 85 val encode_map_encode_tactic : hol_type -> hol_type -> term list * term -> 86 (term list * term) list * (thm list [all...] |
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/arm8/step/ |
H A D | arm8_stepLib.sig | 7 val arm8_names: string list 9 val arm8_step: Term.term -> Thm.thm list 10 val arm8_step_code: string quotation -> Thm.thm list list 11 val arm8_step_hex: string -> Thm.thm list
|
/seL4-l4v-10.1.1/HOL4/src/bag/ |
H A D | bagSimpleLib.sig | 5 val BAG_RESORT_CONV : int list -> conv 7 val GET_BAG_IN_THMS : term -> thm list 10 val get_resort_list___pred : (term -> bool) -> term -> int list 12 val get_resort_lists___pred_pair : (term -> term -> bool) -> term -> term -> (int list * int list)
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/compiler/ |
H A D | codegen_x86Lib.sig | 6 val x86_assign2assembly : codegen_inputLib.assign_type -> string list 7 val x86_guard2assembly : codegen_inputLib.guard_type -> string list * (string * string) 17 val to_x86_regs : unit -> {redex: Term.term, residue: Term.term} list 18 val set_x86_regs : (int * string) list -> unit 19 val get_x86_regs : unit -> (int * string) list
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/ |
H A D | gr-sig.sml | 52 type 'b out = ('b * node) list 72 val matchOrd : node * ''b list * ''b list * ('a,''b) graph -> ('a,''b) decomp 73 val matchOrdFwd : node * ''b list * ('a,''b) graph -> ('a,''b) fwd_decomp 78 val suc : node * ('a,'b) graph -> node list 79 val pred : node * ('a,'b) graph -> node list 81 val gfold : (('a,'b) context -> node list) -> ('a * 'c -> 'd) -> 82 ('d * 'c -> 'c) -> 'c -> node list -> ('a,'b) graph -> 'c 83 val nodes : ('a,'b) graph -> node list 84 val labNodes : ('a,'b) graph -> (node * 'a) list [all...] |
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.1/ |
H A D | gr-sig.sml | 52 type 'b out = ('b * node) list 72 val matchOrd : node * ''b list * ''b list * ('a,''b) graph -> ('a,''b) decomp 73 val matchOrdFwd : node * ''b list * ('a,''b) graph -> ('a,''b) fwd_decomp 78 val suc : node * ('a,'b) graph -> node list 79 val pred : node * ('a,'b) graph -> node list 81 val gfold : (('a,'b) context -> node list) -> ('a * 'c -> 'd) -> 82 ('d * 'c -> 'c) -> 'c -> node list -> ('a,'b) graph -> 'c 83 val nodes : ('a,'b) graph -> node list 84 val labNodes : ('a,'b) graph -> (node * 'a) list [all...] |
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.2/util/ |
H A D | gr-sig.sml | 52 type 'b out = ('b * node) list 72 val matchOrd : node * ''b list * ''b list * ('a,''b) graph -> ('a,''b) decomp 73 val matchOrdFwd : node * ''b list * ('a,''b) graph -> ('a,''b) fwd_decomp 78 val suc : node * ('a,'b) graph -> node list 79 val pred : node * ('a,'b) graph -> node list 81 val gfold : (('a,'b) context -> node list) -> ('a * 'c -> 'd) -> 82 ('d * 'c -> 'c) -> 'c -> node list -> ('a,'b) graph -> 'c 83 val nodes : ('a,'b) graph -> node list 84 val labNodes : ('a,'b) graph -> (node * 'a) list [all...] |
/seL4-l4v-10.1.1/HOL4/examples/diningcryptos/ |
H A D | leakageLib.sig | 9 val UNFOLD_CONV : (thm list) -> (term -> thm) -> conv 15 val LEAKAGE_COMPUTE_PROVE_FINITE : term -> thm list -> thm 16 val LEAKAGE_COMPUTE_FINITE_HLR : term * term * term -> thm list -> thm list 17 val LEAKAGE_COMPUTE_CROSS_NOT_EMPTY : term * term * term -> thm list -> thm 18 val LEAKAGE_COMPUTE_INITIAL_REDUCE : term * term * term -> thm list -> conv 20 val COMPUTE_HLR_CARDS : term * term * term -> (term -> thm) -> (term -> thm) -> (term -> thm) -> (term -> thm) -> (term -> thm) -> (term -> thm) -> thm list 21 val LEAKAGE_COMPUTE_REDUCE_CARDS : term * term * term -> thm list -> (term -> thm) -> (term -> thm) -> (term -> thm) -> (term -> thm) -> (term -> thm) -> (term -> thm) -> conv 22 val LEAKAGE_COMPUTE_HLR_CROSS : term * term * term -> thm list -> (term -> thm) -> (term -> thm) -> (term -> thm) -> (term -> thm) -> (term -> thm) -> (term -> thm) -> conv 23 val LEAKAGE_COMPUTE_IMAGE_HLR_CROSS : term * term * term -> thm list [all...] |
/seL4-l4v-10.1.1/HOL4/examples/HolCheck/ |
H A D | modelTools.sig | 12 val get_trans : model ->(string * Term.term) list 15 val get_vord : model -> string list option 17 val get_props : model -> (string * Term.term) list 18 val get_results : model -> (PrimitiveBddRules.term_bdd * Thm.thm option * Term.term list option) list option 23 val set_trans : (string * Term.term) list -> model -> model 26 val set_vord : string list -> model -> model 28 val set_props : (string * Term.term) list -> model -> model 29 val set_results : (PrimitiveBddRules.term_bdd * Thm.thm option * Term.term list option) list [all...] |