Searched defs:eq (Results 51 - 56 of 56) sorted by relevance
123
| /seL4-l4v-10.1.1/HOL4/src/postkernel/ |
| H A D | Theory.sml | 1101 val eq = mk_thy_const{Name="=",Thy="min",Ty=ty-->ty-->bool} value
1107 val (eq,l) = dest_comb Rator value
|
| /seL4-l4v-10.1.1/HOL4/src/1/ |
| H A D | Drule.sml | 2389 val eq = mk_eq (mk_comb (A, r), mk_comb (A, r')) value
|
| H A D | Prim_rec.sml | 830 val eq = inst [alpha |-> bool] boolSyntax.equality value
873 val eq = inst [alpha |-> bool] boolSyntax.equality value
920 let val eq = FUN_EQ_CONV tm value
1960 val eq = hd (hyp th) value
[all...] |
| /seL4-l4v-10.1.1/HOL4/src/num/theories/ |
| H A D | arithmeticScript.sml | 1805 local val (eq,ls) = value
|
| /seL4-l4v-10.1.1/HOL4/src/quotient/src/ |
| H A D | quotient.sml | 111 val eq = Thm.ALPHA (concl listTheory.list_induction) tm value
2552 val eq = repeat resolve_quotient ith value
4025 val eq = mk_eq(x,y) value
|
| /seL4-l4v-10.1.1/HOL4/src/bool/ |
| H A D | boolScript.sml | 1568 and eq = mk_exists(x,Q) value
1615 val eq = mk_exists(x,Q) value
3951 val eq value
[all...] |
Completed in 212 milliseconds
123