/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Normalize.sig | 24 | 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 D | m0_progLib.sig | 8 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 D | DiskFilesHeader.sig | 6 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 D | DataSize.sig | 7 const_tyopl : (term * (string*string)) list} option
|
/seL4-l4v-10.1.1/HOL4/src/metis/ |
H A D | folTools.sig | 21 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 D | mlibMatch.sig | 14 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 D | Gen_arith.sig | 4 val non_presburger_subterms : Term.term -> Term.term list
|
/seL4-l4v-10.1.1/HOL4/src/prekernel/ |
H A D | Tag.sig | 5 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 D | Cond_rewrite.sig | 15 :(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 D | tttLearn.sig | 6 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 D | Defn.sig | 17 {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 D | BuildCommand.sig | 8 {extra_impl_deps : File list,
|
/seL4-l4v-10.1.1/HOL4/tools/ |
H A D | buildcline.sig | 8 val cline_opt_descrs : t cline_result GetOpt.opt_descr list
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/graph/ |
H A D | file_readerLib.sig | 11 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 D | sequenceTools.sig | 5 val SEQ_CASES_TAC : Term.term frag list -> Abbrev.tactic
|
/seL4-l4v-10.1.1/HOL4/examples/HolBdd/ |
H A D | DerivedBddRules.sig | 24 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 D | Conversion.sig | 6 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 D | Regexp_Match.sig | 9 table : int list list, 10 final : bool list}
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/cheri/step/ |
H A D | cheri_stepLib.sig | 8 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 D | MutRecDef.sig | 21 arg_info : TypeInfo.type_info list}list} list
|
/seL4-l4v-10.1.1/HOL4/src/datatype/mutrec/utils/ |
H A D | elsaUtils.sig | 25 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 D | hol88Lib.sig | 14 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 D | hhReconstruct.sig | 12 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 D | qbuf.sig | 6 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 D | Streams.sig | 10 val stream_append_list : (unit -> 'a stream) list -> (unit -> 'a stream) 12 val permutations : 'a list -> unit -> 'a list stream
|