Searched refs:first (Results 126 - 150 of 742) sorted by relevance

1234567891011>>

/seL4-l4v-master/isabelle/src/Tools/Metis/src/
H A DAtom.sig10 (* A type for storing first order logic atoms. *)
H A DUnits.sml63 first check (LiteralNet.match net lit)
/seL4-l4v-master/HOL4/polyml/
H A DexportPoly.sml51 N.B. polyImport takes the first argument that is not recognised as
/seL4-l4v-master/HOL4/examples/machine-code/graph/
H A Dstack_introLib.sml15 val x = first (can (match_term pat)) ps
/seL4-l4v-master/HOL4/examples/parity/
H A DPARITY_exercisesScript.sml37 (* Specification first:
/seL4-l4v-master/isabelle/src/HOL/Hahn_Banach/document/
H A Droot.tex43 \medskip The document is structured as follows. The first part contains
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/
H A DAtom.sig10 (* A type for storing first order logic atoms. *)
H A DUnits.sml63 first check (LiteralNet.match net lit)
/seL4-l4v-master/l4v/isabelle/src/HOL/Hahn_Banach/document/
H A Droot.tex43 \medskip The document is structured as follows. The first part contains
/seL4-l4v-master/HOL4/src/tfl/src/
H A DDefn.sig65 first theorem should be the equations and the second the induction
/seL4-l4v-master/HOL4/src/real/
H A DrealSimps.sig47 common factor must be the first universally quantified variable in
/seL4-l4v-master/l4v/isabelle/src/HOL/Data_Structures/document/
H A Droot.tex74 They were invented by Crane \cite{Crane72}. A first functional implementation
/seL4-l4v-master/isabelle/src/HOL/Data_Structures/document/
H A Droot.tex74 They were invented by Crane \cite{Crane72}. A first functional implementation
/seL4-l4v-master/HOL4/src/postkernel/
H A DThyDataSexp.sig74 val first : 'a dec list -> 'a dec value
/seL4-l4v-master/HOL4/Manual/LaTeX/
H A Dack.tex42 added material on first order proof search; and Tjark Weber, who wrote
52 and improvement, the \HOL\ logic is unchanged since the first edition
94 sending lists of errors in the first edition. Thanks to everyone who
/seL4-l4v-master/HOL4/src/bag/
H A DbagSimpleLib.sml54 (*add first element again*)
57 (*swap the first two elements*)
70 (*first bring the first element, i.e. n, to the front*)
73 (*remove first element*)
/seL4-l4v-master/HOL4/src/simp/src/
H A DCache.sml34 fun first p [] = raise FIRST function
35 | first p (h::t) = if p h then h else first p t
48 (case snd (first ok prevs) of
347 in this situation should first try conv on the original
/seL4-l4v-master/HOL4/tools/mlyacc/src/
H A Dmklrtable.sml137 (* method for filling tables - first compute the reductions called for in a
143 for reduction by that item. The first reduction is mapped to a list of
309 val {nullable,first} =
317 first=first,
/seL4-l4v-master/HOL4/polyml/modules/
H A DMakefile.in168 first=`echo "$$dir1" | sed -e "$$sed_first"`; \
169 if test "$$first" != "."; then \
170 if test "$$first" = ".."; then \
175 if test "$$first2" = "$$first"; then \
180 dir0="$$dir0"/"$$first"; \
/seL4-l4v-master/seL4/manual/parts/
H A Dbootup.tex28 first slot of the CNode has CPTR 0x0, the second slot has CPTR 0x1 etc.
30 The first 12 slots contain specific capabilities as listed in
87 \texttt{end} being the CPTR of the first slot after the region ends, i.e.\
146 ordered such that the first capability references the first frame of the
/seL4-l4v-master/HOL4/src/pred_set/src/more_theories/
H A DordinalNotationScript.sml438 (* The set of all first exponents of ordinals anywhere in S is n.e. and *)
462 (* element that alpha_1 is the first exponent of. There may be more than one *)
472 (* Now consider the subset of sj where all the ordinals have first exponent *)
484 (* Now we want to consider the set of all first coeff. for any ordinal in *)
506 (* Consider the subset of ordinals in s_alpha_1 that have k_1 as first expt. *)
544 (* Start first case. There is a "d" in Tails with rank <=n. *)
593 (* End first case. *)
/seL4-l4v-master/isabelle/src/Doc/Intro/document/
H A Dgetting.tex23 and demonstrates forward proof. The examples are set in first-order logic.
24 The command to start Isabelle running first-order logic is
172 To illustrate the notation, consider two axioms for first-order logic:
225 resolves the conclusion of $thm1$ with the first premise of~$thm2$.
237 first-order logic.\footnote{For a listing of the FOL rules and their \ML{}
242 first print \tdx{mp}, which is the rule~$({\imp}E)$, then resolve it with
412 first premise by assumption. But \texttt{eresolve_tac} additionally deletes
470 first-order logic. Let us try the example from \S\ref{prop-proof},
502 deviate from~\S\ref{prop-proof} by tackling subgoal~3 first, using
700 first
[all...]
/seL4-l4v-master/l4v/isabelle/src/Doc/Intro/document/
H A Dgetting.tex23 and demonstrates forward proof. The examples are set in first-order logic.
24 The command to start Isabelle running first-order logic is
172 To illustrate the notation, consider two axioms for first-order logic:
225 resolves the conclusion of $thm1$ with the first premise of~$thm2$.
237 first-order logic.\footnote{For a listing of the FOL rules and their \ML{}
242 first print \tdx{mp}, which is the rule~$({\imp}E)$, then resolve it with
412 first premise by assumption. But \texttt{eresolve_tac} additionally deletes
470 first-order logic. Let us try the example from \S\ref{prop-proof},
502 deviate from~\S\ref{prop-proof} by tackling subgoal~3 first, using
700 first
[all...]
/seL4-l4v-master/HOL4/src/metis/
H A DmlibClause.sml432 fun neq_simp1 cl = first (total (dest_neq cl)) (literals cl);
526 necessary) to make the first hit an Id.
531 clause. If M was the largest, then keep the first hit an Id. If N was
532 the largest, then make the first hit a Sym. If in the previous step we
533 had to flip all the hits to make the first hit an Id, then flip this
534 first hit too.
/seL4-l4v-master/HOL4/examples/finite-test-set/
H A Dfinite_test_setScript.sml7 UOK Every first-order formula (in prenex normal form) over the natural numbers is
20 UOK Thus, every first-order formula can be decided by checking a single instance.
21 UOK This sounds surprising at first, until you realise what is not shown: how to

Completed in 271 milliseconds

1234567891011>>