Searched defs:conj (Results 1 - 17 of 17) sorted by path
| /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/arm8/step/ |
| H A D | arm8_stepLib.sml | 745 fun conj th = Drule.LIST_CONJ [thm1, thm2, thm3, th, arm8_exception th] function
|
| /seL4-l4v-10.1.1/HOL4/examples/miller/subtypes/ |
| H A D | subtypeTools.sml | 277 fun conj res [] = res function
|
| /seL4-l4v-10.1.1/HOL4/src/1/ |
| H A D | Drule.sml | 1200 val conj = mk_conj (A1, A2) value
|
| H A D | mp_then.sml | 76 fun conj f t = t |> dest_imp |> #1 |> strip_conj |> f function
|
| /seL4-l4v-10.1.1/HOL4/src/HolSmt/ |
| H A D | Z3_ProofReplay.sml | 540 val conj = boolSyntax.dest_neg lhs value
[all...] |
| /seL4-l4v-10.1.1/HOL4/src/IndDef/ |
| H A D | CoIndDefLib.sml | 70 val conj = mk_conj(conj1, closed') value
|
| /seL4-l4v-10.1.1/HOL4/src/bool/ |
| H A D | boolScript.sml | 1938 val conj = ASSUME ���^t1 /\ ~^t2��� value
2270 val conj = ���$/\��� value
2298 val conj = ���$/\��� and disj = ���$\/��� value
2422 val conj = ���$/\\��� value
2497 val conj = ���$/\\��� value
[all...] |
| /seL4-l4v-10.1.1/HOL4/src/datatype/mutrec/ |
| H A D | Recftn.sml | 673 let val (conj, exists_data2) = value
[all...] |
| /seL4-l4v-10.1.1/HOL4/src/emit/ |
| H A D | ConstMapML.sml | 115 val conj = prim_mk_const{Name="/\\",Thy="bool"} value
|
| /seL4-l4v-10.1.1/HOL4/src/metis/ |
| H A D | mlibTerm.sml | 99 fun conj cs (And (a, b)) = conj (a :: cs) b function
|
| /seL4-l4v-10.1.1/HOL4/src/pattern_matches/ |
| H A D | patternMatchesLib.sml | |
| /seL4-l4v-10.1.1/HOL4/src/portableML/ |
| H A D | UnicodeChars.sig | 111 val conj : string value
|
| H A D | UnicodeChars.sml | 42 val conj = U 0x2227 value
|
| /seL4-l4v-10.1.1/HOL4/src/quotient/examples/ |
| H A D | ind_rel.sml | 1502 let val conj = mk_conj (list_mk_comb (prop_var, vars), value
|
| /seL4-l4v-10.1.1/HOL4/src/real/ |
| H A D | complexScript.sml | 946 val conj = new_definition value
[all...] |
| /seL4-l4v-10.1.1/HOL4/src/simp/src/ |
| H A D | Unwind.sml | 504 let val (conj,value) = find_var_value (hd vars) (strip_conj body) value
[all...] |
| /seL4-l4v-10.1.1/HOL4/src/unwind/ |
| H A D | unwindLib.sml | 754 else let val conj = list_mk_conj l2 value
|
Completed in 213 milliseconds