Searched +refs:aux +refs:diff +refs:aux (Results 1 - 8 of 8) sorted by relevance

/seL4-l4v-master/seL4/manual/
H A DMakefile9 # To create a LaTeX diff against the CVS HEAD revision, use the target
10 # "diff" (or "viewdiff").
58 Optional = $(addsuffix -diff, $(Targets))
94 diff: diff_pdf
221 viewdiff: diff
232 rm -f *.aux *.toc *.bbl *.blg *.dvi *.log *.pstex* *.eps *.cb *.brf \
233 *.out *.ps *-diff.tex *.mps .log *.pdf *.tgz *~ *.lof *.lot env.tex
243 @echo "Main targets: all diff view viewdiff print clean tar"
244 @echo "'make diff' will show changes to head revision"
245 @echo "'make DIFF=<rev> diff' wil
[all...]
/seL4-l4v-master/HOL4/examples/machine-code/graph/
H A DbackgroundLib.sml30 fun diff xs ys = filter (fn x => not (mem x ys)) xs function
46 fun lines aux = case TextIO.inputLine(t) of
47 NONE => rev aux
48 | (SOME line) => lines (line::aux)
98 fun aux k n [] = fail() function
99 | aux k n (x::xs) = if k = x then n else aux k (n+1) xs
100 in aux x 1 xs end
H A Dderive_specsLib.sml74 fun aux t [] = t function
75 | aux t (v::vs) =
76 mk_cond(v,aux (subst [v|->T] t) vs,aux (subst [v|->F] t) vs)
77 in SIMP_CONV std_ss [] (aux tm vs) |> concl |> dest_comb |> snd end
109 fun aux (p:int) (seen:int list) (guard:term) = function
125 (fn n => aux (n:int) (p::seen) (gs:term)) nexts))) ys) end)
133 val result = aux 0 [] T
597 val xs = (diff (assign ~1 (construct_thm_trace res2)) [~1])
/seL4-l4v-master/HOL4/src/pred_set/Manual/
H A DMakefile33 rm -f *.dvi *.aux *.toc *.log *.idx *.ilg *.ps *.pdf theorems.tex
56 ${DOCTOTEX} ${Help}/thms/diff theorems.tex
/seL4-l4v-master/HOL4/src/tfl/src/
H A DDefn.sml143 val diff = Lib.op_set_diff Term.aconv V2 V1 value
147 in if Lib.op_mem Term.aconv Bvar diff
188 fun aux_defn (NESTREC {aux, ...}) = SOME aux
248 | inst_defn (NESTREC{eqs,ind,R,SV,aux,stem}) theta =
253 aux=inst_defn aux theta, stem=stem}
299 | elim_tcs (NESTREC {eqs, ind, R, SV, aux, stem}) thms =
303 aux=elim_tcs aux thm
[all...]
/seL4-l4v-master/HOL4/examples/machine-code/compiler/
H A Dreg_allocLib.sml42 fun diff xs ys = filter (fn y => not (mem y ys)) xs function
162 fun aux tm = let function
184 in TOP_DOWN_CONV aux end
196 fun forward [] aux = []
197 | forward ((x,y)::xs) aux = let
198 val y = list_find y aux handle HOL_ERR _ => y
199 val aux = filter (fn (lhs,rhs) => not (x IN FVs rhs)) aux value
200 in (x,y) :: forward xs ((x,y)::aux) end
/seL4-l4v-master/HOL4/examples/theorem-prover/lisp-runtime/extract/
H A Dlisp_extractLib.sml176 fun aux tm = function
187 in ``If`` $$ aux (rand x1) $$ aux x2 $$ aux x3 end
190 val ys = map (fn (x,y) => pairSyntax.mk_pair(x |> dest_var |> fst |> fromMLstring, aux y)) xs
192 in ``Let`` $$ y $$ (aux x) end
203 val ys = map aux xs
208 in (aux tm2, th) end
381 fun diff xs ys = filter (fn x => not (mem x ys)) xs function
/seL4-l4v-master/HOL4/Manual/Guide/
H A Dguide.tex211 {\tt .aux}, {\tt .toc} and {\tt .log}.
241 suffixes {\tt .dvi}, {\tt .aux}, {\tt .toc}, {\tt .log}, {\tt .idx} and {\tt
327 suffixes {\tt .dvi}, {\tt .aux}, {\tt .toc}, {\tt .log}, {\tt .idx} and {\tt
828 the output, which is from {\tt diff(1)}.

Completed in 139 milliseconds