/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/arm/model/ |
H A D | armAssemblerLib.sig | 4 val arm_code: string quotation -> string list 6 string quotation -> string list * assemblerLib.lines 7 val arm_disassemble: string quotation -> string list
|
/seL4-l4v-10.1.1/HOL4/src/1/ |
H A D | DefnBase.sig | 9 | NONREC of {eqs:thm, ind:thm, SV:term list, stem:string} 10 | STDREC of {eqs:thm list, ind:thm, R:term,SV:term list,stem:string} 11 | MUTREC of {eqs:thm list, ind:thm, R:term,SV:term list, 13 | NESTREC of {eqs:thm list, ind:thm, R:term,SV:term list, 15 | TAILREC of {eqs:thm list, ind:thm, R:term, SV:term list, stem:string} 19 val all_terms : defn -> term list [all...] |
H A D | ConseqConv.sig | 50 val FIRST_CONSEQ_CONV : conseq_conv list -> conseq_conv; 51 val EVERY_CONSEQ_CONV : conseq_conv list -> conseq_conv; 69 val ASM_CONSEQ_CONV_TAC : (thm list -> directed_conseq_conv) -> tactic 125 a theorem "|- t' ==> t" in the preprocessed strengthen list. Then CONSEQ_TOP_REWRITE_CONV 142 val CONSEQ_TOP_REWRITE_CONV : (thm list * thm list * thm list) -> directed_conseq_conv; 143 val CONSEQ_TOP_HO_REWRITE_CONV : (thm list * thm list * thm list) [all...] |
/seL4-l4v-10.1.1/HOL4/src/emit/ |
H A D | ConstMapML.sig | 18 APPEND : 'a list -> 'a list -> 'a list 20 APPEND : char list -> char list -> char list 23 former if you ask for data on APPEND : num list -> num list -> num list. 27 APPEND : num list [all...] |
/seL4-l4v-10.1.1/HOL4/src/quantHeuristics/ |
H A D | quantHeuristicsLibAbbrev.sig | 5 type selection_fun = term -> (term -> int) -> term -> (term * string) list 11 val QUANT_ABBREV_CONV : selection_fun list -> quantHeuristicsLibBase.quant_param list -> conv 12 val QUANT_ABBREV_TAC : selection_fun list -> quantHeuristicsLibBase.quant_param list -> tactic 15 val SIMPLE_QUANT_ABBREV_CONV : selection_fun list -> conv 16 val SIMPLE_QUANT_ABBREV_TAC : selection_fun list -> tactic 20 val select_funs_combine : selection_fun list -> selection_fun 31 val select_fun_match_occ : int -> term frag list -> (term -> string) -> selection_fun 32 val select_fun_match : term frag list [all...] |
/seL4-l4v-10.1.1/HOL4/src/tfl/src/ |
H A D | Induction.sig | 7 : thry -> {fconst : term, R : term, SV : term list, 8 pat_TCs_list: (term * term list) list}
|
/seL4-l4v-10.1.1/HOL4/tools/Holmake/ |
H A D | tailbuffer.sig | 5 val new : {numlines : int, patterns : string list} -> t 7 val output : t -> {fulllines : string list, lastpartial : string, 8 patterns_seen: string list}
|
/seL4-l4v-10.1.1/HOL4/examples/ARM/v4/ |
H A D | arm_rulesLib.sig | 10 val arm_rules : (string * thm) list 12 val RULE_GET : term -> thm list -> thm list
|
/seL4-l4v-10.1.1/isabelle/src/Pure/System/ |
H A D | command_line.scala | 14 private def chunks(list: List[String]): List[List[String]] = 15 list.indexWhere(_ == "\n") match { 16 case -1 => List(list) 18 val (chunk, rest) = list.splitAt(i) 21 def unapplySeq(list: List[String]): Option[List[List[String]]] = Some(chunks(list))
|
/seL4-l4v-10.1.1/HOL4/help/src-sml/ |
H A D | Htmlsigs.sig | 2 val sigsToHtml : string -> string -> string list -> string -> string 3 -> (string * string) list -> string * string -> unit 7 val listDir : string -> string list
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/System/ |
H A D | command_line.scala | 14 private def chunks(list: List[String]): List[List[String]] = 15 list.indexWhere(_ == "\n") match { 16 case -1 => List(list) 18 val (chunk, rest) = list.splitAt(i) 21 def unapplySeq(list: List[String]): Option[List[List[String]]] = Some(chunks(list))
|
/seL4-l4v-10.1.1/HOL4/src/tactictoe/src/ |
H A D | tttSynt.sig | 6 type psubst = (int * int) list 7 type tsubst = (term * term) list 24 val msg_synt : 'a list -> string -> unit 26 val writel_synt : string -> string list -> unit 29 val conjecture : term list -> term list
|
H A D | tttGoallistData.sig | 7 val import_glfea : string list -> unit 8 val update_glfea : int list -> (bool * int) -> unit
|
H A D | tttThmData.sig | 6 type lbl_t = (string * real * goal * goal list) 8 val import_thmfea : string list -> unit
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/arm8/model/ |
H A D | arm8AssemblerLib.sig | 3 val arm8_code: string quotation -> string list 4 val arm8_disassemble: string quotation -> string list
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/riscv/prog/ |
H A D | riscv_progLib.sig | 4 val riscv_spec: Term.term -> Thm.thm list 5 val riscv_spec_hex: string -> Thm.thm list
|
/seL4-l4v-10.1.1/HOL4/src/parse/ |
H A D | GrammarDeltas.sig | 5 type_grammar.delta list * term_grammar.user_delta list
|
/seL4-l4v-10.1.1/HOL4/src/portableML/mosml/concurrent/ |
H A D | Future.sig | 7 val joins : 'a future list -> 'a list
|
/seL4-l4v-10.1.1/HOL4/src/postkernel/ |
H A D | HolKernelDoc.sig | 10 val gen_find_term: (term list * term -> 'a option) -> term -> 'a option 11 val gen_find_terms: (term list * term -> 'a option) -> term -> 'a list 13 (term list * term -> bool) -> (term -> 'a) -> term -> 'a option 19 val disch: term * term list -> term list 22 val find_terms: (term -> bool) -> term -> term list 24 hol_type list -> term set -> term -> term -> 25 {redex: term, residue: int} list * 26 {redex: term, residue: term} list * [all...] |
/seL4-l4v-10.1.1/HOL4/examples/machine-code/graph/ |
H A D | stack_analysisLib.sig | 8 (Thm.thm * int * int option) option) list -> int list
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/ppc/ |
H A D | ppc_Lib.sig | 8 val ppc_test : string -> (string * string) list -> (string * string) list -> thm
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/x86/ |
H A D | x86_Lib.sig | 8 val x86_test : string -> (string * string) list -> (string * string) list -> thm
|
/seL4-l4v-10.1.1/HOL4/examples/acl2/examples/acl2-hol-ltl-paper-example/ |
H A D | load_book.sig | 11 val load_book : (string->unit) -> (thm->thm) -> string -> (string * thm) list list
|
/seL4-l4v-10.1.1/HOL4/src/compute/src/ |
H A D | clauses.sig | 7 | Papp of { Head : term, Args : pattern list} 11 Args : (term * 'a fterm) list, 15 | CLOS of { Env : 'a fterm list, Term : 'a dterm } 20 | App of 'a dterm * 'a dterm list (* order: outermost ahead *) 24 val partition_skip : int option -> (term * 'b fterm) list -> 25 (term * 'b fterm) list * (term * 'b fterm) list 30 Rewrite of rewrite list 40 lhs: pattern list, (* patterns = constant args in lhs of thm *) 47 val from_list : thm list [all...] |
/seL4-l4v-10.1.1/HOL4/src/rational/ |
H A D | schneiderUtils.sig | 10 val ASM_LIST_TAC : int list 11 -> (thm list -> term list * 'a -> 'b) 12 -> term list * 'a -> 'b 13 val ASM_TAC : int -> (thm -> term list * 'a -> 'b) -> term list * 'a -> 'b 32 val MP2_TAC : thm -> goal -> (term list * term) list * (thm list -> thm) 33 val MY_MP_TAC : term -> goal -> (term list * ter [all...] |