Searched refs:list (Results 201 - 225 of 1918) sorted by relevance

1234567891011>>

/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/
H A DNormalize.sig24 | Simplify of thm * thm list
35 thm list -> (Formula.formula * inference * Formula.formula list) list
49 val addCnf : thm -> cnf -> (Thm.clause * thm) list * cnf
51 val proveCnf : thm list -> (Thm.clause * thm) list
53 val cnf : Formula.formula -> Thm.clause list
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/m0/prog/
H A Dm0_progLib.sig8 val m0_spec: string -> Thm.thm list
9 val m0_spec_code: string quotation -> Thm.thm list list
10 val m0_spec_hex: string -> Thm.thm list
/seL4-l4v-10.1.1/HOL4/src/1/
H A DDiskFilesHeader.sig6 datatype pretype = ptv of string | ptop of int * int list
10 type prethm = preterm list * preterm
13 id array * pretype array * pre_vc array * (string * prethm) list
15 val convert_prethms : parse_result -> (string * HolKernel.thm) list
/seL4-l4v-10.1.1/HOL4/src/datatype/
H A DDataSize.sig7 const_tyopl : (term * (string*string)) list} option
/seL4-l4v-10.1.1/HOL4/src/metis/
H A DfolTools.sig21 type vars = term list * hol_type list
39 type fol_problem = {thms : thm1 list, hyps : thm1 list, query : formula1 list}
40 val recent_fol_problems : fol_problem list option ref
49 val build_map : parameters * string list * thm list -> logic_map
53 type Query = vars * term list
54 type Result = vars * thm list
[all...]
H A DmlibMatch.sig14 val matchl : subst -> (term * term) list -> subst
16 val matchl_literals : subst -> (formula * formula) list -> subst
20 val unifyl : subst -> (term * term) list -> subst
23 val unifyl_literals : subst -> (formula * formula) list -> subst
/seL4-l4v-10.1.1/HOL4/src/num/arith/src/
H A DGen_arith.sig4 val non_presburger_subterms : Term.term -> Term.term list
/seL4-l4v-10.1.1/HOL4/src/prekernel/
H A DTag.sig5 val axioms_of : tag -> string Nonce.t list
7 val dest_tag : tag -> string list * string list
15 val read_disk_tag : Dep.depdisk * string list -> tag
/seL4-l4v-10.1.1/HOL4/src/res_quan/src/
H A DCond_rewrite.sig15 :(term -> term -> ((term,term)subst * (hol_type,hol_type)subst) list)
19 :term -> term -> ((term,term)subst * (hol_type,hol_type)subst) list
21 :(term -> term -> ((term,term)subst * (hol_type,hol_type)subst) list)
25 val COND_REWRITE1_CONV : thm list -> thm -> conv
/seL4-l4v-10.1.1/HOL4/src/tactictoe/src/
H A DtttLearn.sig6 type lbl_t = (string * real * goal * goal list)
7 type fea_t = int list
24 val pe_abs : string -> (string * (string * thm) list list)
/seL4-l4v-10.1.1/HOL4/src/tfl/src/
H A DDefn.sig17 {SV : term list,
19 extracta : (thm * term list * bool) list,
20 pats : pattern list,
27 val mk_defns : string list -> term list -> defn list
28 val Hol_defns : string list -> term quotation -> defn list
29 val Hol_multi_defns : term quotation -> defn list
[all...]
/seL4-l4v-10.1.1/HOL4/tools/Holmake/
H A DBuildCommand.sig8 {extra_impl_deps : File list,
/seL4-l4v-10.1.1/HOL4/tools/
H A Dbuildcline.sig8 val cline_opt_descrs : t cline_result GetOpt.opt_descr list
/seL4-l4v-10.1.1/HOL4/examples/machine-code/graph/
H A Dfile_readerLib.sig11 val read_files : string -> string list -> unit
12 val section_body : string -> (int * string * string) list
13 val section_io : string -> int list * int * bool
15 val section_names : unit -> string list
/seL4-l4v-10.1.1/HOL4/examples/miller/formalize/
H A DsequenceTools.sig5 val SEQ_CASES_TAC : Term.term frag list -> Abbrev.tactic
/seL4-l4v-10.1.1/HOL4/examples/HolBdd/
H A DDerivedBddRules.sig24 val traceBack : varmap -> term_bdd list -> thm -> thm -> (term_bdd * (term_bdd * term_bdd) list) list
28 val flatten_pair : term -> term list
29 val BddSatone : term_bdd -> (term_bdd * term_bdd) list
31 val findTrace : varmap -> thm -> thm -> thm -> thm * thm list * thm
34 val computeTrace : (int -> term_bdd -> 'a) -> varmap -> thm -> thm * thm -> term_bdd list
39 val BddSubst : (term_bdd * term_bdd) list -> term_bdd -> term_bdd
42 val extendVarmap : term list -> varmap -> varmap
44 val showVarmap : unit -> (string * int) list
[all...]
/seL4-l4v-10.1.1/HOL4/examples/STE/
H A DConversion.sig6 val base_defn_list : thm list
10 val STE_CONV_RULE : thm -> thm list -> thm
16 val TF : (term * string * term * int * int) list -> term
20 val STE : term -> term -> term -> thm list -> bool -> thm
/seL4-l4v-10.1.1/HOL4/examples/formal-languages/regular/
H A DRegexp_Match.sig9 table : int list list,
10 final : bool list}
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/cheri/step/
H A Dcheri_stepLib.sig8 val cheri_step: Term.term -> Thm.thm list
9 val cheri_step_hex: string -> Thm.thm list
11 val cheri_find_opc: Term.term -> (string * Term.term) list
/seL4-l4v-10.1.1/HOL4/src/datatype/mutrec/
H A DMutRecDef.sig21 arg_info : TypeInfo.type_info list}list} list
/seL4-l4v-10.1.1/HOL4/src/datatype/mutrec/utils/
H A DelsaUtils.sig25 val ADD_ASSUMS_THEN :{new_assumptions:term list, tactic:tactic} -> tactic
26 val ADD_STRIP_ASSUMS_THEN :{new_assumptions:term list, tactic:tactic} ->
30 val ASSUME_LIST_TAC :thm list -> tactic
33 specialization_list:term list} -> thm
41 val REDUCE_TAC :thm list -> tactic
54 val is_contained_in :{subset:term list, superset: term list} -> bool
55 val mapshape :{functions:('a list -> 'b) list,
56 partition:int list,
[all...]
/seL4-l4v-10.1.1/HOL4/src/hol88/
H A Dhol88Lib.sig14 type ('a,'b)hol88subst = ('b * 'a) list
16 val match : term -> term -> (term * term) list * (hol_type * hol_type) list
17 val assoc : ''a -> (''a * 'b) list -> ''a * 'b
18 val rev_assoc : ''a -> ('b * ''a) list -> 'b * ''a
19 val frees : term -> term list
21 val GEN_REWRITE_RULE : (conv -> conv) -> thm list -> thm list -> thm -> thm
22 val GEN_REWRITE_TAC : (conv -> conv) -> thm list -> thm list
[all...]
/seL4-l4v-10.1.1/HOL4/src/holyhammer/
H A DhhReconstruct.sig12 val get_lemmas : (string * string) -> string list option
15 val mk_metis_call : string list -> string
16 val hh_reconstruct : string list -> goal -> (string * tactic)
/seL4-l4v-10.1.1/HOL4/src/parse/
H A Dqbuf.sig6 val new_buffer : 'a HOLPP.frag list -> 'a qbuf
14 val lex_to_toklist : 'a HOLPP.frag list -> 'a base_tokens.base_token locn.located list
/seL4-l4v-10.1.1/HOL4/src/portableML/
H A DStreams.sig10 val stream_append_list : (unit -> 'a stream) list -> (unit -> 'a stream)
12 val permutations : 'a list -> unit -> 'a list stream

Completed in 196 milliseconds

1234567891011>>