Searched refs:first (Results 151 - 175 of 742) sorted by relevance
1234567891011>>
/seL4-l4v-master/HOL4/src/TeX/ |
H A D | holindex-demo.tex | 150 \defHOLtm{term_id_1}{The first term}{SUC a > 0 /\ X > 2} 152 \defHOLty{type_id_1}{The first type}{:bool} 300 \begin{flushright}#3 \ldots$\!$\dotfill #4\end{flushright}{%first line
|
/seL4-l4v-master/HOL4/src/parse/ |
H A D | parse_type.sml | 231 fun tuple_oparrays first rest tuple = 232 case first of 236 raise ERRloc l "array type can't take tuple as first argument"
|
H A D | Preterm.sig | 37 (* Performs the first phase of type-checking, altering the types
|
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/ |
H A D | COPIER.sml | 45 val splitString: string -> { first:string,second:string } 80 (* Process sub-directories first. That way they will be further down the list. *) 102 (* On the first pass we build datatypes, on the second type abbreviations
|
H A D | EXPORTTREESIG.sml | 36 val PTreferences: (bool * location list) -> ptProperties (* The references to the ID. The first is true if this is exported. *)
|
H A D | LEXSIG.sml | 70 (* Construct the location that starts at the start of the first location
|
/seL4-l4v-master/HOL4/examples/boyer_moore/ |
H A D | helper_funcsScript.sml | 106 (* Find first index of element in list. Returns past end of list if no elem *) 183 (* Checking that checkPairs correctly finds first point of mismatch *) 292 to left correctly returning first point of failure *)
|
/seL4-l4v-master/HOL4/src/holyhammer/ |
H A D | hhExportLib.sml | 38 Higher-order to first-order type 154 (* first-order names *) 221 Higher-order theorems in a first-order embedding
|
/seL4-l4v-master/HOL4/examples/hardware/hol88/ |
H A D | binary-trees.ml | 72 % 1) first define Max for the maximum of two numbers. %
|
/seL4-l4v-master/HOL4/examples/hardware/hol88/computer/ |
H A D | computer.ml | 13 % from a register-transfer point of view. It is used in the first %
|
/seL4-l4v-master/HOL4/examples/l3-machine-code/arm/decompiler/ |
H A D | arm_decompLib.sml | 97 mov r3, r0 ; first address
|
/seL4-l4v-master/HOL4/src/1/ |
H A D | match_goal.sig | 59 Iterate over list, taking first thing that works.
|
/seL4-l4v-master/HOL4/src/datatype/mutrec/ |
H A D | Recftn.sml | 23 first term gives explictly the values of the function on all 117 (* first need to deconstruct rec_axiom so we know what to look for *) 185 (#cons(Lib.first (same_cons constructor) gen_cons_data)) 192 * (#cons(Lib.first (same_cons constructor) gen_cons_data))) 212 (* this is the first time we've seen this type *) 497 \<rec vars> <cons args -- nonrecursive ones first>. one *) 537 Our first step will be to get rid of all the unwanted conjuncts 556 (* To prove this lemma we will use TAC_PROOF. Our first task is to 690 This is why we are using lemma1 in the first place *)
|
/seL4-l4v-master/HOL4/src/integer/ |
H A D | CooperMath.sig | 70 Both take the factor as an arbint and as a term as the first two
|
/seL4-l4v-master/HOL4/src/metis/ |
H A D | normalForms.sig | 196 (* Eliminates some lambdas to make terms "as first-order as possible". *)
|
/seL4-l4v-master/HOL4/src/simp/src/ |
H A D | Opening.sig | 7 * The first argument should be a function implementing reflexivity
|
/seL4-l4v-master/HOL4/tools/Holmake/ |
H A D | GetOpt.sig | 40 * RequireOrder: no option processing after first non-option
|
H A D | internal_functions.sig | 56 first such character. If it returns NONE, then there is no such
|
/seL4-l4v-master/HOL4/tools-poly/Holmake/ |
H A D | winNT-systeml.sml | 4 It is the very first thing compiled by the HOL build process so it
|
/seL4-l4v-master/HOL4/tools-poly/poly/ |
H A D | Help.sig | 22 positioning the first occurrence of id at the center of the screen.
|
/seL4-l4v-master/HOL4/examples/ |
H A D | Thery.sml | 68 This leaves two goals. The first is easy to show.
|
/seL4-l4v-master/HOL4/examples/acl2/ml/ |
H A D | acl2encodeLib.sig | 135 (* The first of these functions should be used for simple definitions *) 139 (* The second of these functions should be used when the first fails, *) 215 (* definitions, two tactics must be supplied. The first to prove that the *) 218 (* The first tactic supplied must provide a well-founded relation over *)
|
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/ParseTree/ |
H A D | PRINT_PARSETREE.sml | 555 | Andalso {first, second, ...} => 558 displayParsetree (first, depth - 1), 566 | Orelse {first, second, ...} => 569 displayParsetree (first, depth - 1),
|
/seL4-l4v-master/isabelle/src/Tools/Metis/src/ |
H A D | Formula.sig | 10 (* A type of first order logic formulas. *)
|
H A D | KeyMap.sig | 84 {first : key * 'a -> 'c option,
|
Completed in 207 milliseconds
1234567891011>>