/seL4-l4v-master/HOL4/tools/Holmake/tests/badincludes/ |
H A D | selftest.sml | 26 require_msg (check_result (okres "dir2")) pResult (Mosml.run hm args) "" 30 val _ = inDir "dir3" (t "Bad -I line in c/line to Holmake") ["-I", "../dir2"]
|
/seL4-l4v-master/HOL4/examples/AI_tasks/ |
H A D | mleDiophSynt.sml | 354 val dir2 = dir1 ^ "/" ^ dataset ^ "_uniform"; value 355 val _ = mkDir_err dir2; app (store_result dir2) (number_snd 0 l1'); 360 val dir2 = dir1 ^ "/" ^ dataset ^ "_distance"; value 361 val _ = mkDir_err dir2; app (store_result dir2) (number_snd 0 l2'); 366 val dir2 = dir1 ^ "/" ^ dataset ^ "_tnn"; value 367 val _ = mkDir_err dir2; app (store_result dir2) (number_snd 0 l3'); 377 val dir2 value 383 val dir2 = dir1 ^ "/" ^ dataset ^ "_distance"; value 389 val dir2 = dir1 ^ "/" ^ dataset ^ "_tnn"; value [all...] |
H A D | mleCombinSynt.sml | 402 val dir2 = dir1 ^ "/" ^ dataset ^ "_uniform"; value 403 val _ = mkDir_err dir2; app (store_result dir2) (number_snd 0 l1'); 408 val dir2 = dir1 ^ "/" ^ dataset ^ "_tnn"; value 409 val _ = mkDir_err dir2; app (store_result dir2) (number_snd 0 l2'); 419 val dir2 = dir1 ^ "/" ^ dataset ^ "_uniform"; value 420 val _ = mkDir_err dir2; app (store_result dir2) (number_snd 0 l1); 425 val dir2 value [all...] |
H A D | mleCombinProve.sml | 62 val dir2 = HOLDIR ^ "/examples/AI_tasks/combin_results/test_tnn_nolimit"; 63 fun g i = #read_result ft_extsearch_uniform (dir2 ^ "/" ^ its i); 79 val _ = writel (dir2 ^ "/theorems")
|
H A D | mleDiophProve.sml | 264 val dir2 = HOLDIR ^ "/examples/AI_tasks/dioph_results_nolimit/test_tnn"; 265 fun g i = #read_result ft_extsearch_uniform (dir2 ^ "/" ^ its i); 282 val _ = writel (dir2 ^ "/theorems") (map (minspace o string_of_goal o dest_thm) thml);
|
/seL4-l4v-master/l4v/misc/zsh/ |
H A D | isabelle_session_names.py | 50 for dir2 in roots: 51 sessions += get(dir + '/' + dir2)
|
/seL4-l4v-master/HOL4/tools/Holmake/tests/recursiveclean/ |
H A D | selftest.sml | 18 val testfiles = ["../depchain1/dir3/foo.uo", "../depchain1/dir2/dir1/bar.uo", 19 "../depchain1/dir2/foo"]
|
/seL4-l4v-master/HOL4/polyml/modules/ |
H A D | Makefile.in | 171 dir2=`echo "$$dir0" | sed -e "$$sed_last"`/"$$dir2"; \ 174 first2=`echo "$$dir2" | sed -e "$$sed_first"`; \ 176 dir2=`echo "$$dir2" | sed -e "$$sed_rest"`; \ 178 dir2="../$$dir2"; \ 185 reldir="$$dir2" 505 dir1=$$subdir; dir2="$(distdir)/$$subdir"; \ 508 dir1=$$subdir; dir2 [all...] |
/seL4-l4v-master/isabelle/src/Pure/Admin/ |
H A D | build_polyml.scala | 133 val dir2 = dir1 + Path.explode(platform_64) 134 File.read_dir(dir2).map(entry => dir2.implode + "/" + entry)
|
H A D | build_jdk.scala | 195 dir2 <- other_dirs.iterator 197 val path2 = dir2.resolve(main_dir.relativize(path1))
|
/seL4-l4v-master/l4v/isabelle/src/Pure/Admin/ |
H A D | build_polyml.scala | 133 val dir2 = dir1 + Path.explode(platform_64) 134 File.read_dir(dir2).map(entry => dir2.implode + "/" + entry)
|
H A D | build_jdk.scala | 195 dir2 <- other_dirs.iterator 197 val path2 = dir2.resolve(main_dir.relativize(path1))
|
/seL4-l4v-master/HOL4/polyml/ |
H A D | Makefile.in | 277 dir2=`echo "$$dir0" | sed -e "$$sed_last"`/"$$dir2"; \ 280 first2=`echo "$$dir2" | sed -e "$$sed_first"`; \ 282 dir2=`echo "$$dir2" | sed -e "$$sed_rest"`; \ 284 dir2="../$$dir2"; \ 291 reldir="$$dir2" 866 dir1=$$subdir; dir2="$(distdir)/$$subdir"; \ 869 dir1=$$subdir; dir2 [all...] |
/seL4-l4v-master/isabelle/src/Pure/System/ |
H A D | isabelle_system.scala | 167 def copy_dir(dir1: Path, dir2: Path): Unit = 168 bash("cp -a " + File.bash_path(dir1) + " " + File.bash_path(dir2)).check
|
/seL4-l4v-master/l4v/isabelle/src/Pure/System/ |
H A D | isabelle_system.scala | 167 def copy_dir(dir1: Path, dir2: Path): Unit = 168 bash("cp -a " + File.bash_path(dir1) + " " + File.bash_path(dir2)).check
|
/seL4-l4v-master/HOL4/src/integer/ |
H A D | CooperMath.sml | 678 val (dir1, dir2) = if var_onL < var_onR then (Left, Right) 680 (* dir2 is the side where x will be ending up *) 683 move_terms_from tt dir2 (not o free_in var) 729 case (tt, dir2, negative_numeral) of 739 conv_at dir2 fiddle_negs THENC 740 conv_at dir2 factor_out_over_sum THENC 745 (move_CONV THENC conv_at dir2 collect_terms THENC 748 conv_at dir2 (LAND_CONV REDUCE_CONV) THENC
|
/seL4-l4v-master/HOL4/tools/unicode-grep/ |
H A D | ugrep.sml | 276 \ " ^ CommandLine.name() ^ " [options] dir1 dir2 .. dirn\n\n\ 314 echo " $0 dir1 dir2 .. dirn"
|
/seL4-l4v-master/HOL4/tools/ |
H A D | configure.sml | 27 valid for SML. For example, write "c:/dir1/dir2/mosml", rather 28 than "c:\\dir1\\dir2\\mosml", and certainly DON'T write 29 "c:\dir1\dir2\mosml".
|
/seL4-l4v-master/HOL4/tools-poly/ |
H A D | configure.sml | 27 valid for SML. For example, write "c:/dir1/dir2/mosml", rather 28 than "c:\\dir1\\dir2\\mosml", and certainly DON'T write 29 "c:\dir1\dir2\mosml".
|
/seL4-l4v-master/HOL4/tools/trailing-wspace/ |
H A D | trailingwspace.sml | 179 val uheader = CommandLine.name() ^ " [options] dir1 dir2 ..."
|
/seL4-l4v-master/HOL4/src/bool/ |
H A D | boolScript.sml | 3600 val dir2 = DISCH_ALL (CONJ p_thm (DISCH p q_thm)) value 3602 IMP_ANTISYM_RULE dir1 dir2
|