| /seL4-l4v-10.1.1/HOL4/examples/acl2/ml/ |
| H A D | sexp.ml | 15 val (opr,_) = strip_comb(lhs(concl(SPEC_ALL th))) var
|
| H A D | acl2encodeLib.sml | 1451 val (opr,args) = strip_comb (lhs concl) value
|
| /seL4-l4v-10.1.1/HOL4/examples/HolCheck/ |
| H A D | ctl2muTools.sml | 28 val (opr,args) = HolKernel.strip_comb f; value
|
| H A D | muSyntax.sml | 133 let val (opr,args) = HolKernel.strip_comb mf; value
152 let val (opr,args) = strip_comb f value
175 let val (opr,args) = strip_comb f value
192 let val (opr,args) = strip_comb f value
224 let val (opr,arg value
260 let val (opr,args) = strip_comb f value
275 let val (opr,args) = strip_comb f value
289 let val (opr,args) = strip_comb (List.hd args) value
309 let val (opr,args) = strip_comb f value
328 let val (opr,args) = strip_comb f value
357 let val (opr,args) = HolKernel.strip_comb f value
378 let val (opr,args) = HolKernel.strip_comb f value
430 let val (opr,args) = strip_comb f value
442 let val (opr,args) = strip_comb f value
472 let val (opr,args) = HolKernel.strip_comb mf; value
507 let val (opr,args) = strip_comb mf value
524 let val (opr,args) = strip_comb mf value
[all...] |
| H A D | cacheTools.sml | 440 val (opr,args) = strip_comb mf value
654 val (opr,args) = strip_comb mf value
[all...] |
| H A D | muCheck.sml | 251 val (opr,args) = strip_comb mf value
|
| /seL4-l4v-10.1.1/HOL4/examples/dev/sw/ |
| H A D | cpsSyntax.sml | 69 let val (opr,args) = strip_comb tm value
|
| /seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.1/ |
| H A D | cpsSyntax.sml | 69 let val (opr,args) = strip_comb tm value
|
| /seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.2/ |
| H A D | cpsSyntax.sml | 69 let val (opr,args) = strip_comb tm value
|
| /seL4-l4v-10.1.1/HOL4/src/num/arith/src/ |
| H A D | GenRelNorm.sml | 14 val opr : term value
|
| H A D | NumRelNorms.sml | 153 val opr = leq_tm value
160 val opr = less_tm value
167 val opr = mk_thy_const{Name = "=", Thy = "min", Ty = num --> num --> bool} value
|
| /seL4-l4v-10.1.1/HOL4/src/rational/ |
| H A D | jbUtils.sml | 147 val (opr,lhs) = Term.dest_comb Rator value
|
| /seL4-l4v-10.1.1/HOL4/examples/dev/ |
| H A D | inlineCompile.sml | 142 val (opr,args) = dest_exp tm value
|
| H A D | vsynth.sml | 152 let val (opr, utyl) = dest_type uty value
168 let val (opr, btyl) = dest_type bty value
175 val (opr, argstyl) = dest_type argsty value
|
| H A D | compile.sml | 460 let val (opr,args) = strip_comb tm value
529 val (opr,args) = dest_exp tm value
1695 then let val opr value
[all...] |
| /seL4-l4v-10.1.1/HOL4/src/HolSat/ |
| H A D | def_cnf.sml | 36 let val (opr,args) = strip_comb (concl th) value
40 let val (opr,args) = strip_comb (hd args) value
107 let val (opr,args) = strip_comb tm value
165 val (opr,args) = strip_comb r value
227 let val (opr,args) = strip_comb r value
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/CCS/ |
| H A D | StrongLawsConv.sml | 276 val (opr, opd) = dest_comb tm; value
|
| /seL4-l4v-10.1.1/HOL4/examples/elliptic/swsep/ |
| H A D | swsepLib.sml | 122 val opr = rator (rator pre); value
|
| /seL4-l4v-10.1.1/HOL4/examples/dev/sw2/ |
| H A D | regAlloc.sml | 298 let val (opr,xs) = strip_comb exp value
|
| /seL4-l4v-10.1.1/HOL4/src/lite/ |
| H A D | liteLib.sml | [all...] |
| /seL4-l4v-10.1.1/HOL4/examples/ARM_security_properties/ |
| H A D | ARM_prover_extLib.sml | 22 let val (opr, acs) = value
194 let val (opr, acs) = value
361 val (opr, arg) = value
376 let val (opr, acs) = strip_comb a value
[all...] |
| H A D | ARM_proverLib.sml | 48 let val (opr, acs) = value
319 let val (opr, acs) = value
623 val (opr, arg) = value
643 val (opr, l,r,action) = value
666 let val (opr, acs) = strip_comb a value
743 val (opr, acs) = strip_comb a value
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/muddy/muddyC/buddy/src/ |
| H A D | bddop.c | 1745 BDD bdd_appex(BDD l, BDD r, int opr, BDD var) argument
1811 bdd_appall(BDD l, BDD r, int opr, BDD var) argument
1877 bdd_appuni(BDD l, BDD r, int opr, BDD var) argument
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/muddy/muddyC/ |
| H A D | muddy.c | 276 EXTERNML value mlbdd_bdd_apply(value left, value right, value opr) /* ML */ argument
512 mlbdd_bdd_appall(value left, value right, value opr, value varset) argument
520 mlbdd_bdd_appex(value left, value right, value opr, value varset) argument
|
| /seL4-l4v-10.1.1/HOL4/examples/formal-languages/regular/ |
| H A D | Regexp_Type.sml | 706 fun opr #"*" = "Star" function
[all...] |