/seL4-l4v-master/HOL4/Manual/Description/ |
H A D | version2.tex | 120 In the sections that follow, those new things in Version 2.0 which
|
/seL4-l4v-master/HOL4/Manual/Guide/ |
H A D | guide.tex | 64 beginning sections of this note useful when they wish to typeset the \HOL\ 156 The following sections describe how to obtain typeset versions of each of the 353 sections, based on the `subject matter' of the theorems. The sections 367 are converted into \latex\ sources are given in the sections that follow. 515 sections describe this standard format for \doc\ files and explain the 527 \noindent These are explained below in sections~\ref{thsec} and~\ref{othsec} 703 sections that follow. 1236 In addition to the specific conventions laid down in the preceding sections for
|
/seL4-l4v-master/HOL4/Manual/LaTeX/ |
H A D | ack.tex | 36 Amjad, who developed a model checking library and wrote sections 80 Tom Melham, who wrote the sections describing type definitions, the
|
/seL4-l4v-master/HOL4/Manual/Logic/ |
H A D | semantics.tex | 732 These mechanisms are described in the following sections. They all
|
H A D | syntax.tex | 1018 third is a binder (see \DESCRIPTION's sections on parsing and
|
/seL4-l4v-master/HOL4/Manual/Reference/ |
H A D | preface.tex | 28 % The theorems are listed in the second chapter, roughly grouped into sections
|
/seL4-l4v-master/HOL4/Manual/Translations/IT/Description/ |
H A D | misc.tex | 637 \index{Holmake@\holmake!conditional inclusion of sections}
|
H A D | version2.tex | 120 In the sections that follow, those new things in Version 2.0 which
|
/seL4-l4v-master/HOL4/Manual/Translations/IT/Tutorial/binomial/ |
H A D | binomial.tex | 961 The previous sections have dealt with the material in theory \verb@BINOMIAL@,
|
/seL4-l4v-master/HOL4/Manual/Tutorial/binomial/ |
H A D | binomial.tex | 961 The previous sections have dealt with the material in theory \verb@BINOMIAL@,
|
/seL4-l4v-master/HOL4/examples/machine-code/graph/ |
H A D | func_decompileLib.sml | 142 (* decompile all sections *)
|
/seL4-l4v-master/HOL4/help/src-sml/ |
H A D | ParseDoc.sig | 27 into a list of "sections", as per the datatypes above.
|
H A D | ParseDoc.sml | 255 fun install_doc_part fname sections = 256 case sections of 259 | FIELD("DOC", [TEXT m]) :: ss => sections 264 fun install_structure_part fname sections = let 280 if not (has_struct_section sections) andalso length name_parts = 3 282 insert3 (FIELD("STRUCTURE", [TEXT (full (hd name_parts))])) sections 283 else sections
|
/seL4-l4v-master/HOL4/src/IndDef/Manual/ |
H A D | paper.tex | 75 explain the logical basis for these definitions. The remaining sections
|
/seL4-l4v-master/HOL4/src/pred_set/Manual/ |
H A D | description.tex | 601 The sections that follow describe most of these conversions; the remainder are 602 discussed in later sections of this manual. 1354 described above in sections~\ref{abst} and~\ref{finite} are then activated, and
|
/seL4-l4v-master/HOL4/src/quotient/Manual/ |
H A D | quotient.tex | 414 The next several sections discuss 434 In sections \ref{sigmacalculus} through 1047 \cite[sections 18.2.2.3-5]{GoMe93}. 2697 (see sections \ref{restrictions} and 4654 using the relation operators mentioned in sections
|
/seL4-l4v-master/HOL4/src/res_quan/Manual/ |
H A D | summacs.tex | 94 % The parents and types sections are set in ttlist environment 97 % The constants and infix sections are set in typelist environment. 107 % The Axioms, definitions and theorems sections are set in thmlist environment 142 % \sec{section_name} marks the sections within a theory, e.g., Types, Theorems.
|
/seL4-l4v-master/isabelle/lib/browser/GraphBrowser/ |
H A D | Spline.java | 61 Vector sections; field in class:Spline 74 sections=new Vector(10,10); 92 sections.addElement(s); 98 Enumeration e1=sections.elements();
|
/seL4-l4v-master/isabelle/src/Doc/Functions/document/ |
H A D | intro.tex | 25 section, and consult the remaining sections only when needed.
|
/seL4-l4v-master/isabelle/src/Doc/Intro/document/ |
H A D | advanced.tex | 296 declaration forms are discussed below. There are some more sections 300 object-logics may add further theory sections, for example
|
H A D | foundations.tex | 2 The following sections discuss Isabelle's logical foundations in detail:
|
/seL4-l4v-master/isabelle/src/Doc/Logics_ZF/document/ |
H A D | ZF.tex | 2125 sections are optional. If present, each is specified as a list of
|
/seL4-l4v-master/isabelle/src/Doc/Tutorial/document/ |
H A D | advanced0.tex | 5 yet and which are worth learning. The sections of this chapter are
|
H A D | fp.tex | 282 recursive functions. The first two sections give a structured presentation of
|
H A D | inductive0.tex | 13 context-free grammars. The first two sections are required reading for anybody
|