Searched refs:first (Results 151 - 175 of 742) sorted by relevance

1234567891011>>

/seL4-l4v-master/HOL4/src/TeX/
H A Dholindex-demo.tex150 \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 Dparse_type.sml231 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 DPreterm.sig37 (* Performs the first phase of type-checking, altering the types
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/
H A DCOPIER.sml45 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 DEXPORTTREESIG.sml36 val PTreferences: (bool * location list) -> ptProperties (* The references to the ID. The first is true if this is exported. *)
H A DLEXSIG.sml70 (* Construct the location that starts at the start of the first location
/seL4-l4v-master/HOL4/examples/boyer_moore/
H A Dhelper_funcsScript.sml106 (* 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 DhhExportLib.sml38 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 Dbinary-trees.ml72 % 1) first define Max for the maximum of two numbers. %
/seL4-l4v-master/HOL4/examples/hardware/hol88/computer/
H A Dcomputer.ml13 % 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 Darm_decompLib.sml97 mov r3, r0 ; first address
/seL4-l4v-master/HOL4/src/1/
H A Dmatch_goal.sig59 Iterate over list, taking first thing that works.
/seL4-l4v-master/HOL4/src/datatype/mutrec/
H A DRecftn.sml23 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 DCooperMath.sig70 Both take the factor as an arbint and as a term as the first two
/seL4-l4v-master/HOL4/src/metis/
H A DnormalForms.sig196 (* Eliminates some lambdas to make terms "as first-order as possible". *)
/seL4-l4v-master/HOL4/src/simp/src/
H A DOpening.sig7 * The first argument should be a function implementing reflexivity
/seL4-l4v-master/HOL4/tools/Holmake/
H A DGetOpt.sig40 * RequireOrder: no option processing after first non-option
H A Dinternal_functions.sig56 first such character. If it returns NONE, then there is no such
/seL4-l4v-master/HOL4/tools-poly/Holmake/
H A DwinNT-systeml.sml4 It is the very first thing compiled by the HOL build process so it
/seL4-l4v-master/HOL4/tools-poly/poly/
H A DHelp.sig22 positioning the first occurrence of id at the center of the screen.
/seL4-l4v-master/HOL4/examples/
H A DThery.sml68 This leaves two goals. The first is easy to show.
/seL4-l4v-master/HOL4/examples/acl2/ml/
H A Dacl2encodeLib.sig135 (* 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 DPRINT_PARSETREE.sml555 | 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 DFormula.sig10 (* A type of first order logic formulas. *)
H A DKeyMap.sig84 {first : key * 'a -> 'c option,

Completed in 207 milliseconds

1234567891011>>