Searched refs:first (Results 76 - 100 of 742) sorted by relevance

1234567891011>>

/seL4-l4v-master/HOL4/src/0/
H A DKernelTypes.sml13 * HOL types are somewhat akin to terms in first order logic. *
/seL4-l4v-master/HOL4/src/1/
H A DAC_Sort.sig37 preprocess: applied to all leaf terms as term is first examined.
/seL4-l4v-master/HOL4/src/HolQbf/
H A DQbfConv.sig10 - first order connectives (/\,\/,==>,~)
/seL4-l4v-master/HOL4/src/integer/
H A DinttoTacs.sml31 possible, but if it never occurs, then one of the first two REWR_CONV's
/seL4-l4v-master/HOL4/src/integer/testing/
H A Dreadproblemfile.sig17 v. The very first term read is combined with the initial value v0.
/seL4-l4v-master/HOL4/src/prekernel/
H A Dlocn.sig24 concatenated and given the number of the first fragment; the
/seL4-l4v-master/HOL4/src/simp/src/
H A DCond_rewr.sig31 or if the term does not match the rewrite in the first place.
/seL4-l4v-master/HOL4/tools/Holmake/
H A DSysteml.sig12 (* first argument to these are the name of the desired executable, the
/seL4-l4v-master/HOL4/Manual/Reference/
H A Dpreface.tex26 % The first chapter is an alphabetical sequence of manual entries for all \ML\
/seL4-l4v-master/HOL4/examples/HolCheck/
H A DksScript.sml5 (* make the first argument to the KS type operator be the state one by
/seL4-l4v-master/isabelle/src/Tools/Metis/src/
H A DParse.sig38 val first : ('a -> 'b * 'a) list -> 'a -> 'b * 'a value
H A DSubst.sml12 (* A type of first order logic substitutions. *)
64 (* Applying a substitution to a first order logic term. *)
197 (* Matching for first order logic terms. *)
223 (* Unification for first order logic terms. *)
/seL4-l4v-master/isabelle/src/Doc/Intro/document/
H A Droot.tex41 on first-order logic rather than higher-order logic.
55 \item first-order logic, constructive and classical versions
60 \item the classical first-order sequent calculus, {\sc lk}
91 \index{Isabelle!release history} Isabelle was first distributed in 1986.
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/
H A DParse.sig38 val first : ('a -> 'b * 'a) list -> 'a -> 'b * 'a value
H A DSubst.sml12 (* A type of first order logic substitutions. *)
64 (* Applying a substitution to a first order logic term. *)
197 (* Matching for first order logic terms. *)
223 (* Unification for first order logic terms. *)
/seL4-l4v-master/l4v/isabelle/src/Doc/Intro/document/
H A Droot.tex41 on first-order logic rather than higher-order logic.
55 \item first-order logic, constructive and classical versions
60 \item the classical first-order sequent calculus, {\sc lk}
91 \index{Isabelle!release history} Isabelle was first distributed in 1986.
/seL4-l4v-master/HOL4/polyml/basis/
H A DASN1.sml38 (* Parse the tag and length information to extract the first tag/value pair from the
42 (* Parse the tag and length information to extract the first tag/value pair from the
77 (* Convert the length data. The first byte is either the length itself, if it
103 (* The type is encoded in the top two bits of the first byte. *)
/seL4-l4v-master/HOL4/src/HolSat/sat_solvers/zc2hs/
H A Dzc2hs.cpp22 typedef vector<pair<enum_ty,vector<ClauseId> > > parsed_clauses; // if first=0,1,2,3 then root,CL,VAR,CONF
75 addLit(atoi(stok.c_str()),lits,numvars); // first lit of first clause
300 if ((vartmp[lit>>1]^1)==lit) continue; // a "first" occ of pivot
370 pclauses[ci].first=DONE;
380 pclauses[ci].first=DONE;
389 pclauses[ci].first=DONE;
404 pclauses[ci].first=DONE;
409 switch (pclauses[ci].first) {
492 // first rea
[all...]
/seL4-l4v-master/HOL4/tools/mlyacc/src/
H A Dcoreutils.sml116 by their first symbol. For each first symbol, make sure the item
121 of items produced by a nonterminal, and insert those with a first
190 kept these items sorted by their shift/goto symbol (the first symbol on
202 of closure items which would result from first taking all the closure items
/seL4-l4v-master/HOL4/examples/machine-code/graph/
H A Dgraph_specsLib.sml139 val pc = first (can (match_term pc_pat)) ps
157 val pc = first (can (match_term pc_pat)) ps
167 val y = first (fn tm => aconv x (repeat rator tm)) state_parts
225 val h = first (can (match_term ``var_word "pc" s = w``)) hs
266 val u = first (fn (t,x) => aconv t ret_reg_name) supdate |> snd
283 val rhs = first (fn (t,x) => (aconv t tm2)) supdate |> snd
309 val tag = first (can dest_call_tag) hs
459 first (fn (i,(th,_,_),_) => i = 52) thms
463 val (_,(th1,_,_),SOME (th2,l:int,j:int option)) = first (not o can make_INST) thms
/seL4-l4v-master/isabelle/src/Doc/Tutorial/document/
H A Drules.tex9 predicate logic. The first examples in this chapter will consist of
116 The first is simply \isa{P}, which is trivial, since \isa{P} is among
183 must prove \isa{Q\ \isasymor\ P}\@. Our first step uses the disjunction
186 matches the rule's first premise. It deletes the matching assumption,
187 regards the first premise as proved and returns subgoals corresponding to
190 to get three subgoals, then proving the first by assumption: the other
202 These are the two subgoals returned by \isa{erule}. The first assumes
203 \isa{P} and the second assumes \isa{Q}. Tackling the first subgoal, we
241 \isa{conjunct1} and \isa{conjunct2} --- simply return the first or second half
254 The first proo
[all...]
/seL4-l4v-master/l4v/isabelle/src/Doc/Tutorial/document/
H A Drules.tex9 predicate logic. The first examples in this chapter will consist of
116 The first is simply \isa{P}, which is trivial, since \isa{P} is among
183 must prove \isa{Q\ \isasymor\ P}\@. Our first step uses the disjunction
186 matches the rule's first premise. It deletes the matching assumption,
187 regards the first premise as proved and returns subgoals corresponding to
190 to get three subgoals, then proving the first by assumption: the other
202 These are the two subgoals returned by \isa{erule}. The first assumes
203 \isa{P} and the second assumes \isa{Q}. Tackling the first subgoal, we
241 \isa{conjunct1} and \isa{conjunct2} --- simply return the first or second half
254 The first proo
[all...]
/seL4-l4v-master/isabelle/src/Pure/
H A Dlibrary.scala58 var first = true
60 if (first) {
61 first = false
/seL4-l4v-master/l4v/isabelle/src/Pure/
H A Dlibrary.scala58 var first = true
60 if (first) {
61 first = false
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/CodeTree/X86Code/
H A DX86FOREIGNCALL.sml52 (* Unix X64. The first six arguments are in rdi, rsi, rdx, rcx, r8, r9.
54 Windows X64. The first four arguments are in rcx, rdx, r8 and r9. The rest are
61 Our ML conventions use eax, ebx for the first two arguments in X86/32,
62 rax, ebx, r8, r9, r10 for the first five arguments in X86/64 and
63 rax, rsi, r8, r9 and r10 for the first five arguments in X86/64-32 bit.
225 (* The stack arguments have to be copied first followed by the ebx and finally eax. *)
277 (* X64 on both Windows and Unix take the first arg in xmm0 and the second in xmm1. They are already there. *)
314 (* X64 on both Windows and Unix take the first arg in xmm0 and the second in xmm1. They are already there. *)
316 (* X64 on both Windows and Unix take the first arg in xmm0. On Unix the integer argument is treated
317 as the first argumen
[all...]

Completed in 118 milliseconds

1234567891011>>