Searched refs:first (Results 26 - 50 of 742) sorted by relevance

1234567891011>>

/seL4-l4v-master/HOL4/examples/muddy/muddyC/buddy/src/
H A Dcppext.cxx358 int first; local
366 first = 1;
372 if (!first)
374 first = 0;
424 int ok, first; local
432 first=1;
448 if (!first)
450 first = 0;
H A Dfdd.c113 order will be $x_1,y_1,x_2,y_2,y_3,y_4$. The index of the first
120 RETURN {* The index of the first domain or a negative error code. *}
739 int ok, first; local
747 first=1;
760 if (!first)
762 first = 0;
924 PROTO {* int fdd_intaddvarblock(int first, int last, int fixed) *}
931 int fdd_intaddvarblock(int first, int last, int fixed) argument
939 if (first > last || first <
[all...]
/seL4-l4v-master/l4v/isabelle/src/Pure/Concurrent/
H A Dstandard_thread.scala54 first: Boolean, delay: => Time, log: Logger, event: => Unit)
73 case Some(request) => if (first) false else { request.cancel; true }
101 // delayed event after first invocation
/seL4-l4v-master/HOL4/examples/theorem-prover/milawa-prover/
H A Dcore.lisp65 (ftbl (define-safe ftbl (first def1) (second def1) (third def1))))
232 (equal (first x) 'quote)))
243 por* first second third
271 (let ((lambda-symbol (first (car x)))
337 (cond ((equal (first x) 'pequal*)
341 ((equal (first x) 'pnot*)
344 ((equal (first x) 'por*)
356 (|LOGIC.FMTYPE| (x) (first x))
393 (symbolp (first x))
405 (|LOGIC.METHOD| (x) (first
[all...]
/seL4-l4v-master/HOL4/examples/lambda/barendregt/
H A DstandardisationScript.sml65 `first (seg j i s) = el j s` by SRW_TAC [numSimps.ARITH_ss][first_seg] THEN
189 M i_reduces N = ?s. okpath (labelled_redn beta) s /\ (first s = M) /\
211 RTC (i_reduce1) (first s) (last s)` THEN1 PROVE_TAC [] THEN
217 Q.EXISTS_TAC `first p` THEN
237 M i1_reduces N = ?s. okpath (labelled_redn beta) s /\ (first s = M) /\
401 !r. r IN redex_posns (first p) /\
419 labelled_redn beta x r (first p) ���
440 `el j p = first (drop j p)` by SRW_TAC [][first_drop] THEN
482 !r. r IN redex_posns (first p) /\
485 r' IN redex_posns (first
[all...]
/seL4-l4v-master/HOL4/examples/acl2/tests/inputs/
H A Dcircuit-bisim.lisp28 (and (equal (<- p (first vars))
29 (<- q (first vars)))
42 (if (evaluation-eq st (first states) vars) T
47 (if (evaluation-eq st (first states) vars)
48 (first states)
74 (and (strict-evaluation-p (first states) vars)
79 (and (booleanp (<- st (first vars)))
84 (and (evaluation-p (first states) vars)
97 (and (evaluation-eq-member-p (first m-states) n-states vars)
107 (and (equal (<- s (first labe
[all...]
/seL4-l4v-master/HOL4/src/portableML/poly/
H A DDynarray.sig32 [fromList (xs, d)] returns an array whose first elements are
35 [tabulate(n, f, d)] returns a new array whose first n elements
/seL4-l4v-master/HOL4/src/simp/src/
H A DCache.sig8 Two arguments are needed. The first should determine if a given
20 is to be shown equal to some other value. The extra, first,
H A DboolSimps.sig31 second argument first *)
35 the second argument first *)
/seL4-l4v-master/isabelle/src/Tools/Metis/src/
H A DThm.sig10 (* An abstract type of first order logic theorems. *)
123 (* The literal L must occur in the first theorem, and the literal ~L must *)
H A DProof.sig10 (* A type of first order logic proofs. *)
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/
H A DThm.sig10 (* An abstract type of first order logic theorems. *)
123 (* The literal L must occur in the first theorem, and the literal ~L must *)
H A DProof.sig10 (* A type of first order logic proofs. *)
/seL4-l4v-master/HOL4/polyml/libpolyml/
H A Dsharedata.cpp92 7. Objects at the next depth are first processed to find pointers to objects
163 static void SortRange(PolyObject * *first, PolyObject * *last);
426 POLYUNSIGNED k = j; // Remember the first object that didn't match.
465 // Simple parallel quick-sort. "first" and "last" are the first
467 void DepthVector::SortRange(PolyObject * *first, PolyObject * *last) argument
469 while (first < last)
471 if (last-first <= 100)
474 qsort(first, last-first
[all...]
/seL4-l4v-master/HOL4/examples/PSL/1.01/official-semantics/
H A DRewritesScript.sml90 * Strongly on first posedge.
98 * Weakly on first posedge.
99 * On first posedge, if there is a posedge: [!c U (c /\ f)]
/seL4-l4v-master/seL4/manual/parts/
H A Dnotifications.tex31 of the invoked notification capability. It also unblocks the first
36 to just waking up the first thread waiting on the notification (also see below).
50 \apifunc{seL4\_Signal}{sel4_signal} is invoked, the first queued thread
/seL4-l4v-master/HOL4/examples/fun-op-sem/small-step/
H A Dpath_auxScript.sml117 `!p1 l p2. first (pconcat p1 l p2) = first p1`,
132 (okpath R (pconcat p1 l p2) ��� okpath R p1 ��� okpath R p2 ��� R (last p1) l (first p2))`,
303 unfold (\(p1,p2). (first p1, first p2))
354 `!p1 p2. first (compose_paths p1 p2) = (first p1, first p2)`,
535 first p1 = first p
[all...]
/seL4-l4v-master/HOL4/src/metis/
H A DfolMapping.sig20 {higher_order : bool, (* Application is a first-order function *)
H A DfolTools.sig42 (* Logic maps manage the interface between HOL and first-order logic *)
52 (* A pure interface to the first-order solver: no normalization *)
/seL4-l4v-master/HOL4/Manual/Reference/
H A Dentries-intro.tex13 others will need to be \texttt{load}-ed first.
/seL4-l4v-master/isabelle/src/Pure/Thy/
H A Dthy_element.scala59 def first: Command = in.head
75 val command = in.first
/seL4-l4v-master/isabelle/src/Doc/Tutorial/document/
H A Dinductive0.tex13 context-free grammars. The first two sections are required reading for anybody
/seL4-l4v-master/l4v/isabelle/src/Pure/Thy/
H A Dthy_element.scala59 def first: Command = in.head
75 val command = in.first
/seL4-l4v-master/l4v/isabelle/src/Doc/Tutorial/document/
H A Dinductive0.tex13 context-free grammars. The first two sections are required reading for anybody
/seL4-l4v-master/isabelle/src/Tools/jEdit/src/
H A Dsimplifier_trace_window.scala150 case Some(first) =>
151 val tree = new Simplifier_Trace_Window.Root_Tree(first.parent)
152 Simplifier_Trace_Window.walk_trace(trace.entries, Map(first.parent -> tree))

Completed in 124 milliseconds

1234567891011>>