/seL4-l4v-master/l4v/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))
|
/seL4-l4v-master/HOL4/src/HolSat/sat_solvers/minisat/ |
H A D | Solver.C | 167 // 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 D | preface.tex | 5 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 D | preface.tex | 5 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 D | MATCH_COMPILER.sml | 97 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 D | lalr.sml | 88 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 D | arm_evalLib.sml | 268 (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 D | finite_developmentsScript.sml | 294 ``!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 D | satTools.sml | 33 ** 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 D | description.tex | 58 \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 D | Parse.sml | 53 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 D | Parse.sml | 53 fun first [] _ = raise NoParse function 54 | first (parser :: parsers) input = (parser || first parsers) input;
|
/seL4-l4v-master/HOL4/src/marker/ |
H A D | markerLib.sig | 80 [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 D | mlibUnits.sml | 54 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 D | Norm_bool.sml | 36 (* 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 D | more-examples.tex | 43 and the first order prover. 48 model-elimination style first order prover.
|
/seL4-l4v-master/isabelle/src/Doc/Logics/document/ |
H A D | preface.tex | 17 \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 D | preface.tex | 17 \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 D | goalTree.sml | 29 (* Apply tactic only at first goal in tree. *) 57 (* Find first goal in tree. *)
|
/seL4-l4v-master/HOL4/examples/acl2/tests/inputs/ |
H A D | cone-of-influence.lisp | 33 (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 D | quick.tex | 70 \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 D | cspace.tex | 50 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 D | Tactical.sml | 95 (* 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 D | da.ml | 29 % We first show that ?r q. k=qn+r. This is easy, with r=k and q=0. %
|
H A D | wop.ml | 27 % We first prove that, if there does NOT exist a smallest n such that %
|