/seL4-l4v-10.1.1/HOL4/developers/docfiles/ |
H A D | gen-documented.sh | 14 ls -1 $holdir/help/Docfiles/*.doc | sed 's/.*s\/\([^/]\+\)\.doc/\1/'
|
/seL4-l4v-10.1.1/HOL4/tools/ |
H A D | buildcline.sml | 13 fun from build_theory_graph debug help jobcount kernelspec multithread 18 help = help, 25 fun from' seqname selftest relocbuild multithread kernelspec jobcount help 30 help = help, 37 fun to f {build_theory_graph, debug, help, jobcount, kernelspec, multithread, 40 f build_theory_graph debug help jobcount kernelspec multithread relocbuild 113 {help = "build with experimental kernel", long = ["expk"], short = "", 115 {help [all...] |
H A D | buildcline_dtype.sml | 6 help : bool, 15 { kernelspec = NONE, jobcount = NONE, seqname = NONE, help = false,
|
/seL4-l4v-10.1.1/HOL4/tools-poly/poly/ |
H A D | Help.sig | 2 (* Help -- on-line help functions *) 4 val help : string -> unit value 15 [help s] provides on-line help on the topic indicated by string s. 17 help "lib"; gives an overview of the Moscow ML library. 18 help "id"; provides help on identifier id (case-insensitive). 36 /str cyclically search for string str in help file (case-insensitive) 43 searched for help files. The directories are searched in order, 46 [indexfiles] is a reference to a list of full paths of help ter [all...] |
/seL4-l4v-10.1.1/HOL4/tools/Holmake/ |
H A D | HM_Core_Cline.sml | 9 fun from debug do_logging dontmakes fast help hmakefile holdir includes 16 fast = fast, help = help, hmakefile = hmakefile, holdir = holdir, 30 hmakefile help fast dontmakes do_logging debug = 33 fast = fast, help = help, hmakefile = hmakefile, holdir = holdir, 42 fun to f {debug, do_logging, dontmakes, fast, help, hmakefile, holdir, 47 f debug do_logging dontmakes fast help hmakefile holdir includes 67 help : bool, 93 help [all...] |
/seL4-l4v-10.1.1/l4v/misc/scripts/ |
H A D | gen_isabelle_root.py | 24 help="output file", metavar="FILE") 26 help="input directory", action="append", default=[], 29 help="isabelle session name", metavar="NAME") 31 help="isabelle base session", metavar="NAME") 33 help="additional named session dependency", action="append", default=[], 36 help="ROOT file should compile with \"quick and dirty\" enabled.", variable 40 help="Generate a theory file instead of a ROOT file.") variable
|
H A D | thydeps | 112 help='Directories containing ROOT or ROOTS files (default: .)') 114 help='Show theory files from these directories (default: all)') 116 help='Path to Isabelle system') 118 help='Print relative paths to -b directory (only one dir allowed)') 120 help='Isabelle session names')
|
/seL4-l4v-10.1.1/seL4/libsel4/tools/ |
H A D | invocation_header_gen.py | 166 help='Name of xml file with invocation definitions', required=True) 168 help='Name of file to create', required=True) 170 help='Is this being generated for libsel4?') 173 help='Is this being generated for the arch layer?') 175 help='Is this being generated for the seL4 arch layer?')
|
/seL4-l4v-10.1.1/seL4/manual/tools/libsel4_tools/ |
H A D | invocation_header_gen.py | 166 help='Name of xml file with invocation definitions', required=True) 168 help='Name of file to create', required=True) 170 help='Is this being generated for libsel4?') 173 help='Is this being generated for the arch layer?') 175 help='Is this being generated for the seL4 arch layer?')
|
/seL4-l4v-10.1.1/seL4/tools/ |
H A D | invocation_header_gen.py | 166 help='Name of xml file with invocation definitions', required=True) 168 help='Name of file to create', required=True) 170 help='Is this being generated for libsel4?') 173 help='Is this being generated for the arch layer?') 175 help='Is this being generated for the seL4 arch layer?')
|
/seL4-l4v-10.1.1/HOL4/src/num/arith/Manual/ |
H A D | Makefile | 6 # Pathname to the arith help files 8 Help=../help 13 DOCTOTEXEXE=../../../../help/src/Doc2Tex.exe
|
/seL4-l4v-10.1.1/HOL4/src/num/reduce/Manual/ |
H A D | Makefile | 5 Help=../help 6 DOCTOTEXEXE=../../../../help/src/Doc2Tex.exe
|
/seL4-l4v-10.1.1/l4v/spec/cspec/ |
H A D | mk_umm_types.py | 39 help="C file to parse") 41 help="output filename") 43 help="add Isabelle ROOT or ROOTS file path", action='append')
|
/seL4-l4v-10.1.1/HOL4/tools/Holmake/mosml/ |
H A D | HM_Cline.sml | 63 {help = "don't use HOL's provided basis 2002", long = ["no_basis2002"], 67 {help = "specify Moscow ML's base directory", long = ["mosmldir"], 83 (map (fn {desc,help,short,long} => 84 {desc = mapd desc, help = help, long = long, short = short})
|
/seL4-l4v-10.1.1/HOL4/tools/unicode-grep/ |
H A D | ugrep.sml | 6 fun from chattiness files_wmatches help tests = 8 chattiness = chattiness, files_wmatches = files_wmatches, help = help, 11 fun from' tests help files_wmatches chattiness = 13 chattiness = chattiness, files_wmatches = files_wmatches, help = help, 16 fun to f {chattiness, files_wmatches, help, tests} = 17 f chattiness files_wmatches help tests 35 help : bool, 231 { help [all...] |
/seL4-l4v-10.1.1/HOL4/src/coretypes/pair-Manual/ |
H A D | Makefile | 6 # Pathname to the string help files 8 Help=../help 15 DOCTOTEXEXE=../../../help/src/Doc2Tex.exe
|
/seL4-l4v-10.1.1/HOL4/src/res_quan/Manual/ |
H A D | Makefile | 6 # Pathname to the help files 8 Help=../help 15 DOCTOTEXEXE=../../../help/src-sml/Doc2Tex.exe
|
/seL4-l4v-10.1.1/HOL4/src/string/Manual/ |
H A D | Makefile | 6 # Pathname to the string help files 8 Help=../help 15 DOCTOTEXEXE=../../../help/src/Doc2Tex.exe
|
/seL4-l4v-10.1.1/HOL4/src/unwind/Manual/ |
H A D | Makefile | 6 # Pathname to the unwind help files 8 Help=../help 15 DOCTOTEXEXE=../../../help/src-sml/Doc2Tex.exe
|
/seL4-l4v-10.1.1/HOL4/tools/trailing-wspace/ |
H A D | trailingwspace.sml | 156 datatype cline_record = CR of { quiet : bool, action : action, help : bool} 157 val init = CR {quiet = false, action = Fix, help = false} 158 fun quiet_upd b (CR {action, help, ...}) = 159 CR {action = action, quiet = b, help = help} 160 fun act_upd a (CR {quiet, help, ...}) = 161 CR {action = a, quiet = quiet, help = help} 163 CR {action = action, quiet = quiet, help = b} 167 {short = "h", long = ["help"], des [all...] |
/seL4-l4v-10.1.1/HOL4/examples/miller/prob/ |
H A D | prob_pseudoTools.sml | 17 (* Simple ML functions to help find good parameters for the linear
|
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/ |
H A D | missing | 28 echo 1>&2 "Try '$0 --help' for more information" 45 -h|--h|--he|--hel|--help) 53 -h, --help display this help and exit 74 echo 1>&2 "Try '$0 --help' for more information" 89 case $2 in --version|--help) exit $st;; esac
|
/seL4-l4v-10.1.1/HOL4/polyml/ |
H A D | missing | 28 echo 1>&2 "Try '$0 --help' for more information" 45 -h|--h|--he|--hel|--help) 53 -h, --help display this help and exit 74 echo 1>&2 "Try '$0 --help' for more information" 89 case $2 in --version|--help) exit $st;; esac
|
/seL4-l4v-10.1.1/HOL4/tools/Holmake/poly/ |
H A D | HM_Cline.sml | 116 {help = "specify HOL state", long = ["holstate"], short = "", 118 {help = "thread count (0/none = max h/w count)", short = "", 120 {help = "specify Poly executable", long = ["poly"], short = "", 122 {help = "use poly rather than a HOL heap", long = ["poly_not_hol"], 126 {help = "perform a relocation build", long = ["relocbuild"], short = "", 129 {help = "specify Poly/ML lib directory", long = ["polymllibdir"], 132 {help = "set time limit (in seconds)", long = ["time_limit"], short = "t", 144 (map (fn {desc,help,short,long} => 145 {desc = mapd desc, help = help, lon [all...] |
/seL4-l4v-10.1.1/HOL4/developers/ |
H A D | poly-prehol.sml | 158 " For introductory HOL help, type: help \"hol\";\n" ^ 164 * Set up the help paths. * 165 * Set parameters for parsing and help. * 183 ( hol_use ("help" ++ "src-sml") "Database" 197 fun HELP s = path (HOLDIR ++ "help" ++ s) 203 {file = "help" ++ "Docfiles" ++ "HOL.help", 209 val help = Help.help value [all...] |