| /seL4-l4v-10.1.1/HOL4/examples/HolCheck/ |
| H A D | ksTools.sml | 242 then let val (cs,cs') = (valOf cstate,valOf cstate') value
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/acl2/ml/ |
| H A D | encodeLib.sml | 37 else let val cs = [match (get_source_function_const t "bottom-cons") t] value
602 let val cs = constructors_of t value
620 let val cs = constructors_of t value
1521 val cs = constructors_of t value
1564 val cs = constructors_of t value
1632 let val cs = constructors_of t value
[all...] |
| H A D | functionEncodeLib.sml | 1662 val cs = polytypicLib.constructors_of t handle e => value
2083 val cs = with_exn (map (rand o lhs o concl)) list value
2445 val cs = constructors_of t value
[all...] |
| H A D | polytypicLib.sml | 810 let val cs = constructors_of t value
930 let val cs = (map (repeat rator o rand o lhs o snd o strip_forall) o strip_conj) term value
|
| /seL4-l4v-10.1.1/HOL4/examples/formal-languages/context-free/ |
| H A D | pegLib.sml | 66 val cs = strip_insert (rhs (concl fdom_thm)) value
|
| /seL4-l4v-10.1.1/HOL4/examples/fun-op-sem/ml/ |
| H A D | typeSoundScript.sml | 32 val cs = strip_conj b val c = hd cs value
|
| /seL4-l4v-10.1.1/HOL4/examples/ |
| H A D | hol_dpllScript.sml | 425 val cs = strip_conj t value
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/common/ |
| H A D | Import.sml | 365 val cs = List.map get_cons tys value
|
| H A D | core_decompilerLib.sml | 162 val (cs, l, r) = value
|
| H A D | stateLib.sml | 354 val cs = value
420 val (cs, defs) = ListPair.unzip l value
979 val (cs, ps) = List.partition progSyntax.is_cond ts value
980 val cs = List.map progSyntax.dest_cond cs value
1102 val (cs, ds) = ListPair.unzip cs_ds value
1645 val (cs, vs) = List.partition no_free rs value
[all...] |
| H A D | utilsLib.sml | 1199 val cs = TypeBase.constructors_of ty value
|
| /seL4-l4v-10.1.1/HOL4/examples/lambda/basics/ |
| H A D | nomdatatype.sml | 63 val cs = strip_conj bod value
|
| /seL4-l4v-10.1.1/HOL4/examples/logic/ |
| H A D | foltypesScript.sml | 428 val cs = map (fn i => List.nth(allcs, i)) is value
|
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/compiler/ |
| H A D | compilerLib.sml | 266 val cs = map (fun_const o fst o snd) qs value
|
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/decompiler/ |
| H A D | decompilerLib.sml | 260 val cs = map (fn th => fn tm => value
427 val cs = map extract_code thms value
1228 val cs = dest_tuple c value
1295 val cs = dest_tuple c value
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/graph/ |
| H A D | derive_specsLib.sml | 608 val cs = map extract_code thms value
|
| H A D | exportLib.sml | 230 val cs = filter is_var (list_dest dest_comb pat) value
|
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/hoare-triple/ |
| H A D | helperLib.sml | 1089 val cs = sort (fn x => fn y => get_offset x <= get_offset y) xs value
|
| H A D | tailrecLib.sml | 56 val cs = dest_tuple c value
|
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/just-in-time/ |
| H A D | export_codeLib.sml | 12 val cs = butlast (list_dest pred_setSyntax.dest_insert c) value
|
| H A D | jit_incrementalScript.sml | 2420 val cs = rev (explode name) value
2423 val (cs,n) = primes (cs,0) value
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/lisp/ |
| H A D | export_codeLib.sml | 12 val cs = butlast (list_dest pred_setSyntax.dest_insert c) value
|
| /seL4-l4v-10.1.1/HOL4/examples/muddy/muddyC/buddy/src/ |
| H A D | kernel.c | 173 int bdd_init(int initnodesize, int cs) argument
|
| /seL4-l4v-10.1.1/HOL4/examples/pgcl/src/ |
| H A D | wpTools.sml | 29 val (cs,ths) = FOL_NORM ths value
|
| /seL4-l4v-10.1.1/HOL4/examples/real-to-float/ |
| H A D | daisyLib.sml | 18 val cs = explode " ,\n[]" value
|