| /seL4-l4v-10.1.1/HOL4/src/integer/ |
| H A D | intLib.sml | 19 fun doit (s, t) = function
28 fun doit (s, t) = function
|
| H A D | CooperSyntax.sml | 42 fun doit posp acc tm = let function
57 fun doit posp acc tm = let function
[all...] |
| H A D | IntDP_Munge.sml | 176 val doit = preprocess THENC DP value
|
| /seL4-l4v-10.1.1/l4v/tools/c-parser/testfiles/ |
| H A D | postfixOps.c | 23 void doit(void) function
|
| /seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/testsuite/libffi.call/ |
| H A D | pyobjc-tc.c | 25 int doit(int o, char* s, Point p, Rect r, int last) function
|
| /seL4-l4v-10.1.1/HOL4/tools/ |
| H A D | buildcline.sml | 75 fun doit ires (wn,t) = function
|
| /seL4-l4v-10.1.1/HOL4/tools/Holmake/ |
| H A D | QFRead.sml | 57 fun doit () = function
|
| H A D | parse_glob.sml | 84 fun doit c = function
139 fun doit c = function
149 fun doit c = function
160 fun doit c = function
170 fun doit c = function
[all...] |
| /seL4-l4v-10.1.1/l4v/tools/c-parser/standalone-parser/ |
| H A D | tokenizer.sml | 76 structure Main = struct fun doit args = handle_args [] args end function
|
| H A D | main.sml | 194 fun doit (fname, specs) () = let function
526 fun doit args = function
|
| /seL4-l4v-10.1.1/HOL4/src/1/ |
| H A D | mp_then.sml | 84 fun doit (n:int) = function
98 fun doit ps n = function
|
| /seL4-l4v-10.1.1/HOL4/src/num/arith/src/ |
| H A D | Sub_and_cond.sml | 164 fun doit t = function
226 fun doit t = function
|
| /seL4-l4v-10.1.1/HOL4/src/simp/src/ |
| H A D | selftest.sml | 96 fun doit t = (QCONV (SIMP_CONV bool_ss [Pa_th, Once rwt_th]) t, function
114 fun doit t = QCONV (SIMP_CONV pure_ss [Once rwt_th]) t function
129 fun doit t = QCONV (SIMP_CONV bool_ss [Once rwt_th]) t function
144 fun doit t = QCONV (SIMP_CONV bool_ss []) t function
154 val doit = QCONV (SIMP_CONV (bool_ss ++ combinSimps.COMBIN_ss) value
166 val doit = QCONV (SIMP_CONV (bool_ss ++ SatisfySimps.SATISFY_ss) []) value
175 val doit = ASM_SIMP_TAC bool_ss [] value
199 val doit = QCONV (SIMP_CONV bool_ss [ASSUME TF, ASSUME FT]) value
209 val doit = QCONV (SIMP_CONV (bool_ss ++ CONJ_ss) []) value
[all...] |
| H A D | Traverse.sml | 82 fun doit (context, thms) = let function
|
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/x64_compiler/ |
| H A D | x64_compilerLib.sml | 20 fun doit tm = function
|
| /seL4-l4v-10.1.1/HOL4/src/parse/ |
| H A D | parse_type.sml | 157 fun doit (t,locn) = function
|
| H A D | Preterm.sml | 301 fun doit f_t args = let function
|
| H A D | parse_term.sml | 1380 fun doit (tt, (top_item, top_token), in_vs) = let function
|
| /seL4-l4v-10.1.1/HOL4/Manual/Tools/ |
| H A D | polyscripter.sml | 49 fun doit () = function
|
| /seL4-l4v-10.1.1/HOL4/src/num/ |
| H A D | numLib.sml | 395 fun doit (s, t) = Parse.temp_remove_ovl_mapping s (losety (dest_thy_const t)) function
|
| /seL4-l4v-10.1.1/HOL4/src/portableML/ |
| H A D | OldPP.sml | 181 fun doit s = let function
|
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/compiler/ |
| H A D | compilerLib.sml | 20 fun doit tm = function
|
| /seL4-l4v-10.1.1/HOL4/src/list/src/ |
| H A D | ListConv1.sml | 639 fun doit t = function
|
| /seL4-l4v-10.1.1/HOL4/src/quantHeuristics/ |
| H A D | quantHeuristicsScript.sml | 412 fun doit cL = function
|