/seL4-l4v-10.1.1/HOL4/src/portableML/ |
H A D | Profile.sig | 14 val results : unit -> (string * call_info) list 17 val print_profile_results : (string * call_info) list -> unit 20 val output_profile_results : TextIO.outstream -> (string * call_info) list ->
|
/seL4-l4v-10.1.1/HOL4/src/portableML/monads/ |
H A D | errormonad.sig | 21 val mmap : ('a -> ('b, 'c, 'd) t) -> 'a list -> ('b, 'c list, 'd) t 22 val foldlM : ('e * 'acc -> ('s,'acc,'error)t) -> 'acc -> 'e list ->
|
/seL4-l4v-10.1.1/HOL4/tools/Holmake/ |
H A D | Holmake_tools_dtype.sml | 23 datatype buildcmds = Compile of File list 24 | BuildScript of string * File list 25 | BuildArticle of string * File list
|
/seL4-l4v-10.1.1/HOL4/examples/theorem-prover/lisp-runtime/extract/ |
H A D | lisp_extractLib.sig | 9 val pure_extract_mutual_rec : string list -> tactic option -> thm 15 val deep_embeddings : string -> (thm * thm) list -> thm * thm list
|
/seL4-l4v-10.1.1/HOL4/examples/elliptic/c_output/ |
H A D | c_outputLib.sig | 15 the function main_func. The parameter tests is a list of pairs 16 (f, (arg, res) list). f is the function to be tested, the other list 20 val translate_to_c : string -> string -> thm list -> thm list -> term -> (term * (term * term) list) list -> unit; 24 It generates a random list of word32-pairs with pair_size elements in 29 val generate_word_pair_list : int -> int -> int -> term list
|
/seL4-l4v-10.1.1/HOL4/examples/formal-languages/regular/ |
H A D | Regexp_Type.sig | 11 | Or of regexp list 15 val alphabet : char list 21 val charset_of : char list -> charset 22 val charset_elts : charset -> char list 56 = Ap of string * tree list 63 | Pack of packelt list 65 val tree_parse : substring -> tree list * substring 67 val quote_to_tree : 'a frag list -> tree 73 val fromQuote : 'a frag list -> regexp
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/arm/step/ |
H A D | arm_configLib.sig | 6 val mk_config_terms: string -> term list
|
/seL4-l4v-10.1.1/HOL4/src/1/ |
H A D | Prim_rec.sig | 13 val doms_of_tyaxiom : thm -> hol_type list 20 val type_constructors : thm -> string -> term list 21 val type_constructors_with_args : thm -> string -> term list 31 val define_case_constant : thm -> thm list 40 Similarly, this function returns a list of theorems where each theorem 41 in the list is the cases theorem for a type characterised in the axiom. 44 val prove_cases_thm : thm -> thm list 46 val prove_constructors_distinct : thm -> thm option list 47 val prove_constructors_one_one : thm -> thm option list
|
H A D | Tactical.sig | 16 val THENL : ('a,'b) gentactic * tactic list -> ('a,'b) gentactic 17 val >| : ('a,'b) gentactic * tactic list -> ('a,'b) gentactic 19 val THENL : tactic * tactic list -> tactic 20 val THENL : list_tactic * tactic list -> list_tactic 34 val TACS_TO_LT : tactic list -> list_tactic 64 val ADD_SGS_TAC : term list -> tactic -> tactic 65 val EVERY : tactic list -> tactic 66 val EVERY_LT : list_tactic list -> list_tactic 67 val FIRST : tactic list -> tactic 68 val MAP_EVERY : ('a -> tactic) -> 'a list [all...] |
/seL4-l4v-10.1.1/HOL4/src/TeX/ |
H A D | EmitTeX.sig | 9 val non_type_definitions : string -> (string * thm) list 10 val non_type_theorems : string -> (string * thm) list 11 val datatype_theorems : string -> (string * thm) list 29 val print_theories_as_tex_doc : string list -> string -> unit
|
/seL4-l4v-10.1.1/HOL4/src/datatype/mutrec/ |
H A D | ConsThms.sig | 12 argument_extraction_definitions : (string * thm) list}
|
/seL4-l4v-10.1.1/HOL4/src/metis/ |
H A D | mlibKernel.sig | 18 val dest_thm : thm -> formula list * (inference * thm list) 21 val AXIOM : formula list -> thm 27 val EQUALITY : formula -> int list -> term -> bool -> thm -> thm
|
/seL4-l4v-10.1.1/HOL4/src/parse/ |
H A D | FCNet.sig | 8 val match : term -> 'a t -> 'a list
|
H A D | Pretype_dtype.sml | 6 | Tyop of {Thy:string,Tyop:string, Args: pretype list}
|
H A D | term_tokens.sig | 12 val lex : string list -> 'a qbuf.qbuf -> 'a term_token locn.located option 16 val user_split_ident : string list -> string -> (string * string) 25 val lextest : string list -> string -> 'a term_token list
|
/seL4-l4v-10.1.1/HOL4/src/portableML/poly/ |
H A D | Par_Exn.sml | 10 val make: exn list -> exn 11 val dest: exn -> exn list option 12 val is_interrupted: 'a Exn.result list -> bool 13 val release_all: 'a Exn.result list -> 'a list 14 val release_first: 'a Exn.result list -> 'a list 22 exception Par_Exn of exn list; 23 (*non-empty list with unique identified elements sorted by exn_ord;
|
/seL4-l4v-10.1.1/HOL4/src/quotient/examples/ |
H A D | ind_rel.sig | 9 Term.term list -> (* patterns *) 11 Term.term list (* each term corresponds to a quantified rule *) 13 Term.term list -> (* patterns *) 19 Thm.thm list (* inversion theorems *)
|
/seL4-l4v-10.1.1/HOL4/src/simp/src/ |
H A D | Cache.sig | 23 list of those terms within it that will be treated as variables. 38 val CACHE :(term -> bool) * (thm list->conv) -> (thm list -> conv) * cache 40 val cache_values : cache -> (term * (term list * thm option) list) list 41 val RCACHE : (term -> term list) * (term -> bool) * (thm list -> conv) -> 42 (thm list -> conv) * cache
|
/seL4-l4v-10.1.1/HOL4/tools/Holmake/mosml/ |
H A D | HM_Cline.sig | 10 val option_descriptions : t HM_Core_Cline.cline_result GetOpt.opt_descr list
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/garbage-collectors/ |
H A D | boolTools.sig | 23 val ORELSE_STRENGTHEN_CONV : conv list -> conv; 24 val CONJ_ASSUMPTIONS_STRENGTHEN_CONV : conv -> term list -> conv; 35 val COND_REWRITE_CONV : thm list -> term -> thm 36 val GUARDED_COND_REWRITE_CONV : (term -> bool) -> thm list -> term -> thm
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/x86_64/ |
H A D | x64_Lib.sig | 8 val x64_test : string -> (string * string * string) list -> unit
|
/seL4-l4v-10.1.1/HOL4/examples/miller/formalize/ |
H A D | extra_pred_setTools.sig | 9 val PSET_TAC : Thm.thm list -> Abbrev.tactic
|
/seL4-l4v-10.1.1/HOL4/examples/ARM/v4/ |
H A D | arm_evalLib.sig | 14 val hol_assemble1 : term -> Arbnum.num -> term frag list -> term 15 val hol_assemble : term -> Arbnum.num -> term frag list list -> term 16 val list_assemble : term -> string list -> term 24 val set_registers : term -> term frag list -> term 25 val set_status_registers : term -> term frag list -> term 32 val print_regs : (int * mode) list -> term -> unit 42 val eval_cp : int * term * term * term * term * term -> thm list 45 val eval : int * term * term * term -> thm list
|
/seL4-l4v-10.1.1/HOL4/examples/CCS/ |
H A D | CCSSyntax.sig | 49 val flat_sum : term -> term list 50 val ladd : term -> term list -> term list 51 val FIND_SMD : term list -> term -> term list -> term -> term list * term list 52 val build_sum : term list -> term 53 val sum_to_fun : term list -> term -> term -> term
|
/seL4-l4v-10.1.1/HOL4/examples/acl2/ml/ |
H A D | translateLib.sig | 5 val CHOOSEP_TAC : thm list -> tactic 6 val CHOOSEP : thm list -> term -> thm 17 val strip_cons : term -> term list 24 val DISJ_CASES_UNIONL : thm -> thm list -> thm
|