/seL4-l4v-master/HOL4/src/0/ |
H A D | KernelTypes.sml | 13 * HOL types are somewhat akin to terms in first order logic. *
|
/seL4-l4v-master/HOL4/src/1/ |
H A D | AC_Sort.sig | 37 preprocess: applied to all leaf terms as term is first examined.
|
/seL4-l4v-master/HOL4/src/HolQbf/ |
H A D | QbfConv.sig | 10 - first order connectives (/\,\/,==>,~)
|
/seL4-l4v-master/HOL4/src/integer/ |
H A D | inttoTacs.sml | 31 possible, but if it never occurs, then one of the first two REWR_CONV's
|
/seL4-l4v-master/HOL4/src/integer/testing/ |
H A D | readproblemfile.sig | 17 v. The very first term read is combined with the initial value v0.
|
/seL4-l4v-master/HOL4/src/prekernel/ |
H A D | locn.sig | 24 concatenated and given the number of the first fragment; the
|
/seL4-l4v-master/HOL4/src/simp/src/ |
H A D | Cond_rewr.sig | 31 or if the term does not match the rewrite in the first place.
|
/seL4-l4v-master/HOL4/tools/Holmake/ |
H A D | Systeml.sig | 12 (* first argument to these are the name of the desired executable, the
|
/seL4-l4v-master/HOL4/Manual/Reference/ |
H A D | preface.tex | 26 % The first chapter is an alphabetical sequence of manual entries for all \ML\
|
/seL4-l4v-master/HOL4/examples/HolCheck/ |
H A D | ksScript.sml | 5 (* make the first argument to the KS type operator be the state one by
|
/seL4-l4v-master/isabelle/src/Tools/Metis/src/ |
H A D | Parse.sig | 38 val first : ('a -> 'b * 'a) list -> 'a -> 'b * 'a value
|
H A D | Subst.sml | 12 (* 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 D | root.tex | 41 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 D | Parse.sig | 38 val first : ('a -> 'b * 'a) list -> 'a -> 'b * 'a value
|
H A D | Subst.sml | 12 (* 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 D | root.tex | 41 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 D | ASN1.sml | 38 (* 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 D | zc2hs.cpp | 22 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 D | coreutils.sml | 116 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 D | graph_specsLib.sml | 139 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 D | rules.tex | 9 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 D | rules.tex | 9 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 D | library.scala | 58 var first = true 60 if (first) { 61 first = false
|
/seL4-l4v-master/l4v/isabelle/src/Pure/ |
H A D | library.scala | 58 var first = true 60 if (first) { 61 first = false
|
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/CodeTree/X86Code/ |
H A D | X86FOREIGNCALL.sml | 52 (* 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...] |