/seL4-l4v-master/HOL4/examples/acl2/tests/obsolete/ |
H A D | doit.bash | 8 old_results_dir=$tests_dir/old-results 10 old_logs_dir=$tests_dir/old-logs 14 rm -rf $results_dir $old_results_dir $logs_dir $old_logs_dir diffout diffout.old ; \ 33 if [ -e diffout ]; then mv diffout diffout.old ; fi
|
H A D | doit.csh | 6 set old_results_dir = $tests_dir/old-results 8 set old_logs_dir = $tests_dir/old-logs 12 rm -rf $results_dir $old_results_dir $logs_dir $old_logs_dir diffout diffout.old 31 if (-e diffout) mv diffout diffout.old
|
/seL4-l4v-master/HOL4/examples/acl2/tests/round-trip/ |
H A D | doit | 7 old_results_dir=$round_trip_dir/old-results 9 old_logs_dir=$round_trip_dir/old-logs 14 rm -rf $results_dir $old_results_dir $logs_dir $old_logs_dir diffout diffout.old ; \ 33 if [ -e diffout ]; then mv diffout diffout.old ; fi
|
/seL4-l4v-master/HOL4/examples/acl2/tests/ |
H A D | doit | 8 old_results_dir=$tests_dir/old-results 10 old_logs_dir=$tests_dir/old-logs 26 rm -f diffout diffout.old 2> /dev/null ; \ 51 if [ -e diffout ]; then mv diffout diffout.old ; fi
|
/seL4-l4v-master/HOL4/src/quotient/src/ |
H A D | quotient.sig | 25 (* is isomorphic to the equivalence classes of the old type. *) 27 (* HOL logic to translate between the old and new types in both *) 53 string -> (* name of abstraction function from old to new *) 54 string -> (* name of representation function from new to old *) 225 func : Term.term, (* old function, to be lifted *) 249 Thm.thm list -> (* old functions are well-defined to respect the 252 as lifted from instanciations on old types, 256 Thm.thm -> (* theorem (regarding old functions) to be lifted *) 293 (* func - term, the old term which is to be lifted *) 296 (* respects - list of theorems asserting that the old function [all...] |
/seL4-l4v-master/HOL4/src/postkernel/ |
H A D | ThyDataSexp.sig | 22 Thus, if the theory data is a list of values, both old and new should be 30 val alist_merge : {old: t, new : t} -> t 31 val append_merge : {old : t, new : t} -> t 34 merge : {old : t, new : t} -> t,
|
/seL4-l4v-master/HOL4/src/AI/sml_inspection/ |
H A D | smlRedirect.sml | 40 (dup2{old = fd, new = stdout}; stack := fd :: !stack) 59 fd :: _ => (dup2{old = fd, new = stdout}; true) 60 | [] => (dup2{old = duplicate_stdout, new = stdout}; false))
|
/seL4-l4v-master/HOL4/src/prekernel/ |
H A D | stringfindreplace.sml | 78 fun newcellf inv old = 79 if inv then old 82 NONE => old 84 (i, (t, Option.map (fn v => (v,1)) (valueOf t)))::old
|
H A D | Globals.sig | 24 val old : string -> string value
|
H A D | Globals.sml | 142 val old = value 146 fn s => String.concat ["old", Int.toString (!c), "->", s, "<-old"] before
|
H A D | locn.sig | 31 claim the new token is near where the old one was *)
|
/seL4-l4v-master/HOL4/polyml/ |
H A D | install-sh | 459 old=`LC_ALL=C ls -dlL "$dst" 2>/dev/null` && 462 set X $old && old=:$2:$4:$5:$6 && 465 test "$old" = "$new" && 477 # Now remove or move aside any old file at destination location.
|
/seL4-l4v-master/HOL4/polyml/libpolyml/ |
H A D | gc_copy_phase.cpp | 278 PolyWord *old = src->wordAddr(bitno); /* Old object address */ local 280 PolyObject *obj = (PolyObject*)(old+1); 292 // into later spaces but that doesn't work well if we have converted old 313 // Update src->upperAllocPtr, so the old object doesn't get trampled. 314 if (old < src->upperAllocPtr) 315 src->upperAllocPtr = old;
|
H A D | sharedata.cpp | 600 PolyWord GetNewAddress(PolyWord old); 617 PolyWord ProcessFixupAddress::GetNewAddress(PolyWord old) argument 619 if (old.IsTagged() || old == PolyWord::FromUnsigned(0)) 620 return old; // Nothing to do. 622 ASSERT(old.IsDataPtr()); 624 PolyObject *obj = old.AsObjPtr(); 640 return old; 643 return old; 669 POLYUNSIGNED AddPolyWordToDepthVectors(PolyWord old); 696 AddPolyWordToDepthVectors(PolyWord old) argument [all...] |
/seL4-l4v-master/HOL4/src/parse/ |
H A D | term_pp_utils.sml | 32 getbvs >- (fn old => setbvs (HOLset.addList(old,bvlist))) 50 (fn old => setbvs (HOLset.addList(old,newbvs)) >> 51 p >- (fn pres => setbvs old >> return pres)) 63 (fn old => fupdate (set true) >> p >- 64 (fn pval => fupdate (set old) >> return pval))
|
/seL4-l4v-master/HOL4/src/boss/theory_tests/ |
H A D | comp_delbinding1Script.sml | 20 (* now replace "foo_def" binding with something else; the old binding
|
/seL4-l4v-master/isabelle/src/Tools/jEdit/src/ |
H A D | pretty_tooltip.scala | 58 val (old, rest) = 63 old.foreach(_.hide_popup) 136 case Some((old, _ :: rest)) => 141 old.foreach(_.hide_popup)
|
/seL4-l4v-master/l4v/isabelle/src/Tools/jEdit/src/ |
H A D | pretty_tooltip.scala | 58 val (old, rest) = 63 old.foreach(_.hide_popup) 136 case Some((old, _ :: rest)) => 141 old.foreach(_.hide_popup)
|
/seL4-l4v-master/isabelle/src/Pure/Admin/ |
H A D | build_release.scala | 407 mv "$DIST_NAME" "${DIST_NAME}-old" 410 mv "${DIST_NAME}-old/README" "${DIST_NAME}-old/NEWS" "${DIST_NAME}-old/ANNOUNCE" \ 411 "${DIST_NAME}-old/COPYRIGHT" "${DIST_NAME}-old/CONTRIBUTORS" "$DIST_NAME" 413 mv "${DIST_NAME}-old/doc/"*.pdf \ 414 "${DIST_NAME}-old/doc/"*.html \ 415 "${DIST_NAME}-old/doc/"*.css \ 416 "${DIST_NAME}-old/do [all...] |
/seL4-l4v-master/l4v/isabelle/src/Pure/Admin/ |
H A D | build_release.scala | 407 mv "$DIST_NAME" "${DIST_NAME}-old" 410 mv "${DIST_NAME}-old/README" "${DIST_NAME}-old/NEWS" "${DIST_NAME}-old/ANNOUNCE" \ 411 "${DIST_NAME}-old/COPYRIGHT" "${DIST_NAME}-old/CONTRIBUTORS" "$DIST_NAME" 413 mv "${DIST_NAME}-old/doc/"*.pdf \ 414 "${DIST_NAME}-old/doc/"*.html \ 415 "${DIST_NAME}-old/doc/"*.css \ 416 "${DIST_NAME}-old/do [all...] |
/seL4-l4v-master/HOL4/examples/muddy/muddyC/buddy/src/ |
H A D | kernel.c | 387 RETURN {* The old number of allocated variables or a negative error code. *} 503 it is called with {\tt oldsize} being the old nodetable size and 537 RETURN {* The old threshold on succes, otherwise a negative error code. *} 542 int old = bddmaxnodeincrease; local 548 return old; 565 RETURN {* The old threshold on succes, otherwise a negative error code. *} 572 int old = bddmaxnodesize; local 574 return old; 596 RETURN {* The old threshold on succes, otherwise a negative error code. *} 601 int old local [all...] |
H A D | cppext.cxx | 199 RETURN {* The old handler *} 204 bddstrmhandler old = strmhandler_bdd; local 206 return old; 523 RETURN {* The old handler *} 528 bddstrmhandler old = strmhandler_fdd; local 530 return old;
|
/seL4-l4v-master/HOL4/src/metis/ |
H A D | mlibPatricia.sml | 76 | Leaf (j,old) => if j = k then Leaf (k, f old)
|
/seL4-l4v-master/HOL4/polyml/mlsource/ |
H A D | BuildAll.sml | 37 line to start the new shell will be in the buffer of the old
|
H A D | BuildBasis.sml | 25 compiled into that rather than the old space. *)
|