/seL4-l4v-master/HOL4/examples/muddy/muddyC/buddy/src/ |
H A D | cppext.cxx | 358 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 D | fdd.c | 113 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 D | standard_thread.scala | 54 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 D | core.lisp | 65 (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 D | standardisationScript.sml | 65 `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 D | circuit-bisim.lisp | 28 (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 D | Dynarray.sig | 32 [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 D | Cache.sig | 8 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 D | boolSimps.sig | 31 second argument first *) 35 the second argument first *)
|
/seL4-l4v-master/isabelle/src/Tools/Metis/src/ |
H A D | Thm.sig | 10 (* 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 D | Proof.sig | 10 (* A type of first order logic proofs. *)
|
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Thm.sig | 10 (* 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 D | Proof.sig | 10 (* A type of first order logic proofs. *)
|
/seL4-l4v-master/HOL4/polyml/libpolyml/ |
H A D | sharedata.cpp | 92 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 D | RewritesScript.sml | 90 * 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 D | notifications.tex | 31 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 D | path_auxScript.sml | 117 `!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 D | folMapping.sig | 20 {higher_order : bool, (* Application is a first-order function *)
|
H A D | folTools.sig | 42 (* 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 D | entries-intro.tex | 13 others will need to be \texttt{load}-ed first.
|
/seL4-l4v-master/isabelle/src/Pure/Thy/ |
H A D | thy_element.scala | 59 def first: Command = in.head 75 val command = in.first
|
/seL4-l4v-master/isabelle/src/Doc/Tutorial/document/ |
H A D | inductive0.tex | 13 context-free grammars. The first two sections are required reading for anybody
|
/seL4-l4v-master/l4v/isabelle/src/Pure/Thy/ |
H A D | thy_element.scala | 59 def first: Command = in.head 75 val command = in.first
|
/seL4-l4v-master/l4v/isabelle/src/Doc/Tutorial/document/ |
H A D | inductive0.tex | 13 context-free grammars. The first two sections are required reading for anybody
|
/seL4-l4v-master/isabelle/src/Tools/jEdit/src/ |
H A D | simplifier_trace_window.scala | 150 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))
|