Searched refs:Help (Results 1 - 22 of 22) sorted by relevance

/seL4-l4v-master/HOL4/src/pred_set/Manual/
H A DMakefile8 Help=../help macro
42 ${DOCTOTEXEXE} ${Help}/entries entries.tex
48 cat ${Help}/thms/mem/*.doc >> theorems.tex
50 ${DOCTOTEX} ${Help}/thms/emuniv theorems.tex
52 ${DOCTOTEX} ${Help}/thms/subs theorems.tex
54 ${DOCTOTEX} ${Help}/thms/unin theorems.tex
56 ${DOCTOTEX} ${Help}/thms/diff theorems.tex
58 ${DOCTOTEX} ${Help}/thms/disj theorems.tex
60 ${DOCTOTEX} ${Help}/thms/insdel theorems.tex
62 ${DOCTOTEX} ${Help}/thm
[all...]
/seL4-l4v-master/HOL4/src/num/arith/Manual/
H A DMakefile8 Help=../help macro
34 ${DOCTOTEXEXE} ${Help}/entries entries.tex
/seL4-l4v-master/HOL4/src/num/reduce/Manual/
H A DMakefile5 Help=../help macro
21 ${DOCTOTEXEXE} ${Help}/entries entries.tex
/seL4-l4v-master/HOL4/src/coretypes/pair-Manual/
H A DMakefile8 Help=../help macro
38 ${DOCTOTEXEXE} ${Help}/entries entries.tex
44 /bin/sh ${DOCTOTEX} ${DOCTOTEXSED} ${Help}/thms theorems.tex
/seL4-l4v-master/HOL4/src/res_quan/Manual/
H A DMakefile8 Help=../help macro
39 ${DOCTOTEXEXE} ${Help}/entries entries.tex
46 /bin/sh ${DOCTOTEX} ${DOCTOTEXSED} ${Help}/thms theorems.tex
/seL4-l4v-master/HOL4/src/string/Manual/
H A DMakefile8 Help=../help macro
38 ${DOCTOTEXEXE} ${Help}/entries entries.tex
44 /bin/sh ${DOCTOTEX} ${DOCTOTEXSED} ${Help}/thms theorems.tex
/seL4-l4v-master/HOL4/src/unwind/Manual/
H A DMakefile8 Help=../help macro
42 ${DOCTOTEXEXE} ${Help}/entries entries.tex
/seL4-l4v-master/HOL4/developers/
H A Dpoly-prehol.sml184 ; hol_use ("tools-poly" ++ "poly") "Help"
200 ( Help.indexfiles := HELP "HOL.Help" :: !Help.indexfiles
201 ; Help.helpdirs := HOLDIR :: SIGOBJ :: !Help.helpdirs
202 ; Help.specialfiles :=
205 title = "HOL Overview"} :: !Help.specialfiles
206 ; Help.displayLines := 60
209 val help = Help
[all...]
H A Dprehol.sml111 val () = indexfiles := HELP "HOL.Help" :: !indexfiles
113 val () = Help.specialfiles :=
116 :: !Help.specialfiles
125 val _ = Help.displayLines := 60;
/seL4-l4v-master/HOL4/tools-poly/poly/
H A DHelp.sml1 structure Help :> Help = struct structure
3 (* Help -- a simple Moscow ML library browser, PS 1995-04-30, 2000-04-22
34 along with Help.
198 raise Fail ("Help.readFile: help file `" ^ file ^ "' not found")
220 handle OS.SysErr _ => raise Fail "Help.showFile: inconsistent help database"
250 fun display sought [] = raise Fail "Help.display"
H A DHelp.sig1 signature Help = sig signature
2 (* Help -- on-line help functions *)
/seL4-l4v-master/HOL4/tools/
H A Dmake_iss.sml31 val _ = FileSys.remove (fullPath ["help", "HOL.Help"])
33 val _ = print "help/HOL.Help, "
H A Dbuildutils.sml799 if (print "Building Help DB\n"; SYSTEML cmd2) then ()
/seL4-l4v-master/HOL4/polyml/mlsource/extra/Win/
H A DMessageBox.sml118 val MB_HELP = 0wx00004000 (* Help Button *)
/seL4-l4v-master/HOL4/help/src-sml/
H A Dmakebase.sml58 val helpfileDef = normPath[HOLpath, "help","HOL.Help"]
/seL4-l4v-master/HOL4/examples/separationLogic/src/holfoot/poly/
H A Dholfoot_command_line.sml38 val _ = print_with_style [Bold] "Help:\n";
/seL4-l4v-master/HOL4/Manual/Tutorial/
H A Dintro.tex46 {\tt help} & Help files for \HOL{} system & Directory\\
/seL4-l4v-master/HOL4/polyml/mlsource/extra/Win/Examples/
H A DmlEdit.sml88 val _ = AppendMenu(menu, [], MenuHandle helpMenu, MFT_STRING "&Help")
/seL4-l4v-master/HOL4/src/compute/src/
H A DcomputeLib.sml422 Help for building up compsets and creating new compset based conversions
/seL4-l4v-master/HOL4/examples/l3-machine-code/common/
H A DutilsLib.sml1090 (* Help prove theorems of the form:
/seL4-l4v-master/HOL4/Manual/Translations/IT/Description/
H A Dmisc.tex20 \section{Help}
18 \\end{itemize} section
/seL4-l4v-master/HOL4/Manual/Description/
H A Dmisc.tex20 \section{Help}
18 \\end{itemize} section

Completed in 301 milliseconds