/seL4-l4v-master/HOL4/src/quantHeuristics/ |
H A D | quantHeuristicsTools.sig | 6 val TOP_ONCE_REWRITE_CONV : thm list -> conv; 24 val VARIANT_TAC : term list -> tactic 25 val VARIANT_CONV : term list -> conv 29 val list_variant : term list -> term list -> (term list * (term,term) Lib.subst);
|
/seL4-l4v-master/l4v/tools/autocorres/tests/examples/ |
H A D | heap_wrap.c | 19 struct list { struct 21 struct list *p; 60 int f8(struct list *l, struct thing *t)
|
/seL4-l4v-master/HOL4/src/IndDef/ |
H A D | IndDefLib.sig | 6 val term_of : term quotation -> term * locn.locn list 7 val term_of_absyn : Absyn.absyn -> term * locn.locn list 14 (term * locn.locn list) -> thm * thm * thm 22 val thy_monos : string -> thm list 24 type rule_induction_map = ({Thy:string,Name:string},thm list) Binarymap.dict 25 val thy_rule_inductions : string -> thm list
|
/seL4-l4v-master/HOL4/examples/formal-languages/regular/ |
H A D | Regexp_Type.sig | 8 val alphabet : char list 14 val charset_of : char list -> charset 15 val charset_elts : charset -> char list 28 | Or of regexp list 50 val catlist : regexp list -> regexp 51 val strip_cat : regexp -> regexp list 52 val dots : int -> regexp list 53 val mk_or : regexp list -> regexp 57 = Ap of string * tree list 65 val tree_parse : substring -> tree list * substrin [all...] |
/seL4-l4v-master/HOL4/src/TeX/theory_tests/ |
H A D | mdtScript.sml | 7 val _ = type_abbrev_pp("string", ``:char list``) 16 | Tyapp of type_op => type list type 24 | Defined of num => (string # term) list => term
|
/seL4-l4v-master/HOL4/src/bag/ |
H A D | bagLib.sig | 21 val list_mk_union : term list -> term 29 val list_mk_insert : term list * term -> term 32 val strip_union : term -> term list 50 val mk_bag : term list * hol_type -> term 51 val strip_insert : term -> term list * term 52 val dest_bag : term -> term list * hol_type 59 val SBAG_SOLVE : thm list -> term -> thm 62 val BAG_RESORT_CONV : int list -> conv 64 val GET_BAG_IN_THMS : term -> thm list 68 val get_resort_list___pred : (term -> bool) -> term -> int list [all...] |
/seL4-l4v-master/HOL4/src/finite_maps/ |
H A D | patriciaLib.sig | 19 val add_list : term_ptree -> (num * term) list -> term_ptree 21 val traverse : term_ptree -> num list 22 val keys : term_ptree -> num list 30 val ptree_of_list : (num * term) list -> term_ptree 31 val list_of_ptree : term_ptree -> (num * term) list 32 val ptree_of_nums : num list -> term_ptree 36 val int_add_list : term_ptree -> (int * term) list -> term_ptree 40 val int_ptree_of_list : (int * term) list -> term_ptree 41 val ptree_of_ints : int list -> term_ptree 45 val string_add_list : term_ptree -> (string * term) list [all...] |
/seL4-l4v-master/HOL4/src/meson/src/ |
H A D | mesonLib.sig | 20 val GEN_MESON_TAC : int -> int -> int -> thm list -> tactic 21 val MESON_TAC : thm list -> tactic 22 val ASM_MESON_TAC : thm list -> tactic
|
/seL4-l4v-master/HOL4/src/metis/ |
H A D | mlibSolver.sig | 20 type solver = formula list -> thm list option stream 31 val solve : solver -> int -> formula list -> thm list list 32 val find : solver -> formula list -> thm list option 40 thms : thm list, (* Context, assumed consistent *) 41 hyps : thm list} (* Hypothesis, or set of support *) 62 val combine : (cost_fn * solver_node) list [all...] |
H A D | mlibUnits.sig | 17 val addl : thm list -> units -> units 20 val prove : units -> formula list -> thm list option
|
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-master/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-master/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-master/HOL4/tools/Holmake/ |
H A D | Holmake_tools_dtype.sml | 23 Compile of 'dep list * 'extra 24 | BuildScript of string * 'dep list * 'extra 25 | BuildArticle of string * 'dep list * 'extra
|
/seL4-l4v-master/HOL4/src/AI/proof_search/ |
H A D | psBigSteps.sig | 12 type 'a rlex = ('a * real list) list 29 val run_bigsteps : ('a,'b) bsobj -> 'a -> bool * 'a rlex * ('a,'b) node list
|
/seL4-l4v-master/HOL4/src/portableML/monads/ |
H A D | errormonad.sig | 22 val mmap : ('a -> ('b, 'c, 'd) t) -> 'a list -> ('b, 'c list, 'd) t 23 val foldlM : ('e * 'acc -> ('s,'acc,'error)t) -> 'acc -> 'e list ->
|
/seL4-l4v-master/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-master/HOL4/examples/l3-machine-code/arm/step/ |
H A D | arm_configLib.sig | 6 val mk_config_terms: string -> term list
|
/seL4-l4v-master/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
|
/seL4-l4v-master/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-master/HOL4/src/datatype/mutrec/ |
H A D | ConsThms.sig | 12 argument_extraction_definitions : (string * thm) list}
|
/seL4-l4v-master/HOL4/src/parse/ |
H A D | Pretype_dtype.sml | 6 | Tyop of {Thy:string,Tyop:string, Args: pretype list}
|
H A D | term_tokens.sig | 13 val lex : string list -> 'a qbuf.qbuf -> 'a term_token locn.located option 17 val user_split_ident : string list -> string -> (string * string) 24 val lextest : string list -> string -> 'a term_token list
|
/seL4-l4v-master/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-master/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 *)
|