Searched +refs:aux +refs:diff +refs:aux (Results 1 - 8 of 8) sorted by relevance
/seL4-l4v-master/seL4/manual/ |
H A D | Makefile | 9 # 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 D | backgroundLib.sml | 30 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 D | derive_specsLib.sml | 74 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 D | Makefile | 33 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 D | Defn.sml | 143 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 D | reg_allocLib.sml | 42 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 D | lisp_extractLib.sml | 176 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 D | guide.tex | 211 {\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