| /seL4-l4v-10.1.1/HOL4/examples/HolCheck/ |
| H A D | lzConv.sml | 259 val {lhs,rhs} = dest_eq (concl th) value
1353 let val {lhs,rhs} = dest_eq tm value
1566 let val {lhs,rhs} = dest_eq tm value
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/acl2/examples/M1/ |
| H A D | sexp.sml | 236 val (lhs,rhs) = dest_eq (spec_all hd_eqn) value
|
| /seL4-l4v-10.1.1/HOL4/examples/acl2/examples/acl2-hol-ltl-paper-example/ |
| H A D | sexp.sml | 236 val (lhs,rhs) = dest_eq (spec_all hd_eqn) value
|
| /seL4-l4v-10.1.1/HOL4/examples/acl2/ml/ |
| H A D | sexp.sml | 236 val (lhs,rhs) = dest_eq (spec_all hd_eqn) value
|
| /seL4-l4v-10.1.1/HOL4/examples/countable/ |
| H A D | countableLib.sml | 30 val lhs = mk_comb(lhs0, c) value
|
| /seL4-l4v-10.1.1/HOL4/examples/dev/sw/ |
| H A D | IR.sml | 179 val (lhs, rest) = dest_pabs var; value
|
| H A D | regAllocation.sml | 857 val (lhs, rest) = dest_pabs lt; value
858 val lhs = subst rules lhs value
885 val (lhs, res value
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.1/ |
| H A D | IR.sml | 170 val (lhs, rest) = dest_pabs var; value
|
| H A D | regAllocation.sml | 857 val (lhs, rest) = dest_pabs lt; value
858 val lhs = subst rules lhs value
885 val (lhs, res value
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.2/ |
| H A D | IR.sml | 170 val (lhs, rest) = dest_pabs lt; value
|
| H A D | regAllocation.sml | 857 val (lhs, rest) = dest_pabs lt; value
858 val lhs = subst rules lhs value
885 val (lhs, res value
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/elliptic/c_output/ |
| H A D | c_outputLib.sml | 348 val (lhs, body) = pairLib.dest_pabs body; value
|
| /seL4-l4v-10.1.1/HOL4/examples/elliptic/swsep/ |
| H A D | swsepScript.sml | 60 let val (lhs,rhs) = dest_eq t value
|
| /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/common/ |
| H A D | core_decompilerLib.sml | 513 val (lhs, rhs) = dest_eq tm value
|
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/acl2/ |
| H A D | m1_progLib.sml | 80 val lhs = hh tm (dest_tuple input) value
|
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/compiler/ |
| H A D | reg_allocLib.sml | 213 val (lhs,rhs) = dest_eq x value
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/decompiler/ |
| H A D | decompilerLib.sml | 1195 val (lhs,rhs) = hd xs value
1271 val (lhs,rhs) = hd xs value
1352 val (lhs,rhs) = (dest_imp o concl) th value
|
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/graph/ |
| H A D | exportLib.sml | 335 val (lhs,rhs) = lemma |> concl |> dest_eq value
|
| H A D | func_decompileLib.sml | 40 val lhs = mk_var(name,type_of rhs) value
190 val (lhs,rhs) = dest_eq goal value
210 val lhs = mk_var(name,type_of rhs) value
|
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/hoare-triple/ |
| H A D | helperLib.sml | 634 val lhs = fst (dest_eq (concl imp)) value
650 val lhs = mk_star(last vs,frame) value
1131 val lhs value
[all...] |
| H A D | tailrecLib.sml | 22 val (lhs,rhs) = hd xs value
107 val (lhs,rhs) = dest_eq tm value
154 val (lhs,rhs) = dest_eq tm value
|
| /seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/tools/ |
| H A D | tuerk_tacticsLib.sml | 13 let val (lhs,rhs) = dest_eq t value
28 let val (lhs,rhs) = dest_eq t value
79 let val (lhs,rhs) = dest_eq t value
90 let val (lhs,rhs) = dest_eq t value
100 let val (lhs,rhs) = dest_eq t value
112 let val (lhs,rhs) = dest_eq t value
165 val (lhs, rhs) = dest_eq (concl thm) value
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/translations/ |
| H A D | translationsLib.sml | 930 val lhs = rand (rator (concl imp_thm)) value
|
| /seL4-l4v-10.1.1/HOL4/examples/theorem-prover/lisp-runtime/extract/ |
| H A D | lisp_extractLib.sml | 404 val lhs = foldl (fn (x,y) => mk_comb(y,x)) new_fun params value
492 val lhs = map (fn x => mk_comb(new_fun,x)) ps value
746 val lhs = foldl (fn (x,y) => mk_comb(y,x)) new_fun params value
774 val lhs value
914 val lhs = foldl (fn (x,y) => mk_comb(y,x)) new_fun params value
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/theorem-prover/lisp-runtime/implementation/ |
| H A D | lisp_compiler_opScript.sml | 2063 val (lhs,rhs) = hd xs value
2082 val (lhs,rh value
[all...] |