| /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...] |