/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 4 val printHTMLBase : string [all...] |
H A D | Symbolic.sig | 3 val unsymb : string -> string 4 val tosymb : string -> string
|
/seL4-l4v-10.1.1/HOL4/src/tactictoe/src/ |
H A D | tttOpen.sig | 4 val core_theories : string list 5 val theory_files : string -> string list 6 val find_heapname : string -> string 7 val find_genscriptdep : string -> string list 8 val run_buildheap : bool -> string -> unit 9 val run_rm_script : bool -> string -> unit 12 val tactictoe_cleanstruct : string [all...] |
H A D | tttNumber.sig | 5 val number_stac : string -> string 6 val drop_numbering : string list -> string list 7 val replace_at : string list * string list -> string list -> string list
|
H A D | tttLexer.sig | 4 val rm_comment : string -> string 5 val ttt_lex : string -> string list
|
/seL4-l4v-10.1.1/HOL4/src/portableML/ |
H A D | UnicodeChars.sig | 5 val alpha : string 6 val beta : string 7 val gamma : string 8 val delta : string 9 val zeta : string 10 val eta : string 11 val theta : string 12 val kappa : string 13 val lambda : string 14 val mu : string [all...] |
H A D | UTF8.sig | 4 exception BadUTF8 of string 5 val getChar : string -> ((string * int) * string) option 6 val lastChar : string -> (string * int) option 7 val size : string -> int 8 val chr : int -> string (* May raise Chr *) 9 val padRight : char -> int -> string -> string [all...] |
/seL4-l4v-10.1.1/HOL4/examples/machine-code/compiler/ |
H A D | codegen_armLib.sig | 6 val arm_assign2assembly : codegen_inputLib.assign_type -> string list 7 val arm_guard2assembly : codegen_inputLib.guard_type -> string list * (string * string) 9 val arm_cond_code : Parse.term -> string * string 10 val arm_conditionalise : string -> string -> string 11 val arm_remove_annotations : string [all...] |
H A D | codegen_ppcLib.sig | 6 val ppc_assign2assembly : codegen_inputLib.assign_type -> string list 7 val ppc_guard2assembly : codegen_inputLib.guard_type -> string list * (string * string) 9 val ppc_cond_code : Parse.term -> string * string 10 val ppc_conditionalise : string -> string -> string 11 val ppc_remove_annotations : string [all...] |
H A D | codegen_x64Lib.sig | 6 val x64_assign2assembly : codegen_inputLib.assign_type -> string list 7 val x64_guard2assembly : codegen_inputLib.guard_type -> string list * (string * string) 9 val x64_cond_code : Parse.term -> string * string 10 val x64_conditionalise : string -> string -> string 11 val x64_remove_annotations : string [all...] |
H A D | codegen_x86Lib.sig | 6 val x86_assign2assembly : codegen_inputLib.assign_type -> string list 7 val x86_guard2assembly : codegen_inputLib.guard_type -> string list * (string * string) 9 val x86_cond_code : Parse.term -> string * string 10 val x86_conditionalise : string -> string -> string 11 val x86_remove_annotations : string [all...] |
/seL4-l4v-10.1.1/HOL4/examples/machine-code/x64_compiler/ |
H A D | x64_codegen_x64Lib.sig | 6 val x64_assign2assembly : x64_codegen_inputLib.assign_type -> string list 7 val x64_guard2assembly : x64_codegen_inputLib.guard_type -> string list * (string * string) 9 val x64_cond_code : Parse.term -> string * string 10 val x64_conditionalise : string -> string -> string 11 val x64_remove_annotations : string [all...] |
/seL4-l4v-10.1.1/HOL4/src/parse/ |
H A D | GrammarSpecials.sig | 4 val fnapp_special : string 5 val bracket_special : string 6 val vs_cons_special : string 7 val resquan_special : string 8 val let_special : string 9 val letcons_special : string 10 val letnil_special : string 11 val and_special : string 12 val fakeconst_special : string 14 {original : KernelSig.kernelname option, fake : string} [all...] |
/seL4-l4v-10.1.1/HOL4/src/prekernel/ |
H A D | stringfindreplace.sig | 4 val subst : {redex:string,residue:string} list -> string -> string
|
H A D | Feedback.sig | 3 type error_record = {origin_structure : string, 4 origin_function : string, 5 message : string} 8 val mk_HOL_ERR : string -> string -> string -> exn 9 val mk_HOL_ERRloc : string -> string -> locn.locn -> string -> exn 10 val wrap_exn : string [all...] |
/seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/ppc/ |
H A D | ppc_Lib.sig | 5 val ppc_decode : string -> thm 6 val ppc_step : string -> thm 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 | 5 val x86_decode : string -> thm 6 val x86_step : string -> thm 8 val x86_test : string -> (string * string) list -> (string * string) list -> thm
|
/seL4-l4v-10.1.1/HOL4/tools/Holmake/ |
H A D | Holdep.sig | 4 exception Holdep_Error of string 5 val main : { assumes : string list, 6 includes : string list, 7 diag : (unit -> string) -> unit, 8 fname : string } -> 9 {tgt : string, deps : string list} 11 val encode_for_HOLMKfile : {tgt : string, deps : string list} -> string [all...] |
H A D | holpathdb.sig | 4 val lookup_holpath : {vname : string} -> string option 5 val extend_db : {vname: string, path : string} -> unit 6 val reverse_lookup : {path : string} -> string 7 val subst_pathvars : string -> string 9 val search_for_extensions : (string -> string lis [all...] |
/seL4-l4v-10.1.1/HOL4/src/holyhammer/ |
H A D | hhWriter.sig | 7 string -> 8 (string -> (string * thm) * string -> bool) -> 9 string list -> 12 string -> 13 (string -> (string * thm) * string -> bool) -> 14 (string * th [all...] |
/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 5 val print_arm8_code: string quotation -> unit 6 val print_arm8_disassemble: string quotation -> unit
|
/seL4-l4v-10.1.1/HOL4/src/1/ |
H A D | ThmSetData.sig | 5 val new_exporter : string -> 6 (string -> (string * Thm.thm) list -> unit) -> 7 {dest : data -> (string * Thm.thm) list option, 8 export : string -> unit, 9 mk : string list -> data * (string * Thm.thm) list} 11 val new_storage_attribute : string -> unit 12 val store_attribute : {attribute: string, thm_name : string} [all...] |
/seL4-l4v-10.1.1/HOL4/src/bool/ |
H A D | TexTokenMap.sig | 4 val TeX_notation : {hol: string, TeX : string * int} -> unit 5 val temp_TeX_notation : {hol: string, TeX : string * int} -> unit 7 val the_map : unit -> (string,string * int)Binarymap.dict
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/x86_64/ |
H A D | x64_Lib.sig | 5 val x64_decode : string -> thm 6 val x64_step : string -> thm 8 val x64_test : string -> (string * string * string) list -> unit
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/x64/model/ |
H A D | x64AssemblerLib.sig | 3 val x64_code: string quotation -> string list 4 val x64_code_no_spaces: string quotation -> string list 5 val x64_disassemble1: string -> string 6 val x64_disassemble_string: string -> (string * string) list 7 val x64_disassemble_term: Term.term -> (string * strin [all...] |