Searched refs:first (Results 51 - 75 of 742) sorted by relevance

1234567891011>>

/seL4-l4v-master/l4v/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))
/seL4-l4v-master/HOL4/src/HolSat/sat_solvers/minisat/
H A DSolver.C167 // Can assume everything has been propagated! (esp. the first two literals are != l_False, unless
168 // the clause is binary and satisfied, in which case the first literal is true)
247 class lastToFirst_lt { // Helper class to 'analyze' -- order literals from last to first occurance in 'trail[]'.
410 | making assumptions). If 'skip_first' is TRUE, the first literal of 'confl' is ignored (needed
523 Lit first = c[0];
524 sconfl = sign(first);
525 lbool val = value(first);
543 assert(unit_id[var(first)] == ClauseId_NULL || value(first) == l_False); // (if variable already has 'id', it must be with the other polarity and we should have derived the empty clause here)
544 if (value(first) !
[all...]
/seL4-l4v-master/isabelle/src/Doc/
H A Dpreface.tex5 Most theorem provers support a fixed logic, such as first-order or
14 classical first-order logic.
48 These include first-order logic (intuitionistic and classical), the sequent
70 impatient to get started, you might skip the first chapter, which
89 on a first reading.
94 Isabelle was first distributed in 1986. The 1987 version introduced a
124 book. Nipkow wrote the first versions of \S\ref{sec:defining-theories},
/seL4-l4v-master/l4v/isabelle/src/Doc/
H A Dpreface.tex5 Most theorem provers support a fixed logic, such as first-order or
14 classical first-order logic.
48 These include first-order logic (intuitionistic and classical), the sequent
70 impatient to get started, you might skip the first chapter, which
89 on a first reading.
94 Isabelle was first distributed in 1986. The 1987 version introduced a
124 book. Nipkow wrote the first versions of \S\ref{sec:defining-theories},
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/ParseTree/
H A DMATCH_COMPILER.sml97 on one of the fields first, and then on the others. The aim is to
120 fun first (PatSet p) = hd p; function
140 else if first a = first b then first a ::: (next a plus next b)
141 else if first a < first b then first a ::: (next a plus b)
142 else first b ::: (a plus next b);
147 else if i = first
[all...]
/seL4-l4v-master/HOL4/tools/mlyacc/src/
H A Dlalr.sml88 val addLookahead = fn {graph,nullable,first,eop,
117 given by the number of symbols before the place. The place before the first
241 (* find first item of the form A -> x .B y, where y =*=> epsilon and
292 NTL.insert((n,Look.union(data,first t)),r)
293 | NONE => NTL.insert ((n,first t),r))
349 whose closure is being taken (i.e. first(y) for an item j of the
407 add_nonterm_lookahead to each such B, and then merges first(y) into
417 let val first_y = first y
438 (* first take care of kernal items. Add the end-of-parse symbols to
/seL4-l4v-master/HOL4/examples/ARM/v7/eval/
H A Darm_evalLib.sml268 (fn ((r1,r2), (first,n)) =>
269 (if term_eq r1 r2 then first else
270 (out [if first then "Registers:\t" else "\t\t", rname n,
279 (fn ((r1,r2), (first,n)) =>
280 (if term_eq r1 r2 then first else
281 (out [if first then "PSRs:\t\t" else "\t\t", psrname n,
290 (fn (tm,first) =>
293 (out [if first then "Memory:\t\t[" else "\t\t[",
295 | _ => first) true l; ()
/seL4-l4v-master/HOL4/examples/lambda/barendregt/
H A Dfinite_developmentsScript.sml294 ``!p. first (strip_path_label p) = strip_label (first p)``,
458 let x = first q in
462 let y' = lift_redn M' r (first t) in
470 pcons M' r (h (lift_redn M' r (first p)) p))``,
482 ``!M' p. first (lift_path M' p) = M'``,
489 ``!p M'. okpath (labelled_redn beta) p /\ (strip_label M' = first p) ==>
495 (strip_label M' = first y)` THEN
499 (?x r p'. (q2 = pcons x r p') /\ labelled_redn beta x r (first p') /\
508 ``!M' p. okpath (labelled_redn beta) p /\ (first
[all...]
/seL4-l4v-master/HOL4/src/HolSat/
H A DsatTools.sml33 ** after the first occurrence of s1 and ends just before the first
34 ** occurrence of s2 that is after the first occurrence of s1
/seL4-l4v-master/HOL4/src/num/reduce/Manual/
H A Ddescription.tex58 \item If the first numeral is zero, we need only specialize the first
65 \item If the first numeral is not zero, then we call the conversion
/seL4-l4v-master/isabelle/src/Tools/Metis/src/
H A DParse.sml53 fun first [] _ = raise NoParse function
54 | first (parser :: parsers) input = (parser || first parsers) input;
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/
H A DParse.sml53 fun first [] _ = raise NoParse function
54 | first (parser :: parsers) input = (parser || first parsers) input;
/seL4-l4v-master/HOL4/src/marker/
H A DmarkerLib.sig80 [stmark_conjunct P t] finds the first conjunct c amongst the
85 [stmark_disjunct P t] finds the first disjunct d amongst the
106 [move_conj_left P t] first looks for a conjunct satisfying P, marks it,
/seL4-l4v-master/HOL4/src/metis/
H A DmlibUnits.sml54 case first (total check) (N.unify uns lit) of NONE => NONE
110 case first (fn lit => uprove uns [lit]) (clause th) of
/seL4-l4v-master/HOL4/src/num/arith/src/
H A DNorm_bool.sml36 (* the conversion takes as its first argument. *)
53 (* atoms are specified by a predicate (first argument). When a negation has *)
/seL4-l4v-master/HOL4/Manual/Tutorial/
H A Dmore-examples.tex43 and the first order prover.
48 model-elimination style first order prover.
/seL4-l4v-master/isabelle/src/Doc/Logics/document/
H A Dpreface.tex17 \texttt{ZF} is built on \texttt{FOL} (first-order logic), both are described
44 \item[\thydx{LK}] is classical first-order logic as a sequent calculus.
/seL4-l4v-master/l4v/isabelle/src/Doc/Logics/document/
H A Dpreface.tex17 \texttt{ZF} is built on \texttt{FOL} (first-order logic), both are described
44 \item[\thydx{LK}] is classical first-order logic as a sequent calculus.
/seL4-l4v-master/HOL4/src/proofman/
H A DgoalTree.sml29 (* Apply tactic only at first goal in tree. *)
57 (* Find first goal in tree. *)
/seL4-l4v-master/HOL4/examples/acl2/tests/inputs/
H A Dcone-of-influence.lisp33 (set-union (find-variables (first equation-list))
38 (set-union (find-variables* (<- equations (first vars)))
88 (if (equal e (first x))
90 (cons (first x) (del e (rest x))))))
216 (first vars)
217 (<- equations (first vars))))))
221 ((memberp (first x) (rest x)) (remove-duplicate-occurrences (rest x)))
222 (t (cons (first x) (remove-duplicate-occurrences (rest x))))))
227 (first vars)
228 (<- init (first var
[all...]
/seL4-l4v-master/HOL4/Manual/Quick/
H A Dquick.tex70 \hol{Tactical}{THEN1} & applies the second tactic to first sub-goal \\
71 \hol{Tactical}{ORELSE} & applies second tactic only if the first fails \\
83 \hol{Tactical}{POP_ASSUM} \var{thm-tactic} & use first assumption \\
86 \hol{Tactical}{FIRST_X_ASSUM} \var{thm-tactic} & use first successful assum. \\
98 \hol{mesonLib}{MESON_TAC} [\var{thms}] & first-order prover \\
100 \holnoref{metisLib}{METIS_TAC} [\var{thms}] & new first-order prover \\
146 \hol{boolSimps}{bool_ss} & propositional and first-order logic simplifications, plus beta-conversion \\
195 \hol{Conv}{GSYM} \var{thm} & reverses the first equation(s) encountered in a top-down search \\
240 \hol{Conv}{ONCE_DEPTH_CONV} & applies conversion once to the first suitable sub-term in top-down order \\
252 \hol{Conv}{ORELSEC}(\var{conv},\var{conv}) & applies the first o
[all...]
/seL4-l4v-master/seL4/manual/parts/
H A Dcspace.tex50 addressing capabilities within them. This chapter first discusses
101 one from the second specified slot to the first, and one from the
102 third to the second. The first and third specified slots may be the
130 index into the \obj{CNode} at which the first capability will be placed.
152 When an object is first created, the initial capability that refers to
223 covered by their own untyped caps, both are children of the first
266 itself, by swapping the capability with the first capability in the
276 deletion requires user-level to delete the tree leaf first if
289 complete in two specific circumstances. The first being where a
339 userspace thread, the kernel first consult
[all...]
/seL4-l4v-master/HOL4/src/1/
H A DTactical.sml95 (* first argument can be a tactic or a list-tactic *)
138 (* first argument can be a tactic or a list-tactic *)
196 (* first argument can be a tactic or a list-tactic *)
205 * first subgoal of tac1
214 [] => raise ERR "THEN1" "goal completely solved by first tactic"
219 else raise ERR "THEN1" "first subgoal not solved by second tactic"
258 first n goals, and ltacb to the rest
272 * A list_tactic that moves the first n goals to the end of the goal list
273 * first n goals
289 * if the first conjunc
[all...]
/seL4-l4v-master/HOL4/examples/hardware/hol88/mos-count/
H A Dda.ml29 % We first show that ?r q. k=qn+r. This is easy, with r=k and q=0. %
H A Dwop.ml27 % We first prove that, if there does NOT exist a smallest n such that %

Completed in 273 milliseconds

1234567891011>>