Searched defs:lhs (Results 76 - 80 of 80) sorted by relevance
1234
| /seL4-l4v-10.1.1/HOL4/src/1/ |
| H A D | Drule.sml | 562 val (lhs, rhs) = dest_eq (concl th) value
642 val (lhs, rhs) = dest_eq (concl th) value
[all...] |
| H A D | Prim_rec.sml | 225 let val (lhs, rhs) = dest_eq t value
358 val (lhs,_) = dest_eq eqn value
876 let val (lhs,rh value
949 let val (lhs,rhs) = dest_eq(snd(strip_forall tm)) value
1286 let val (lhs,rhs) = (dest_eq o #2 o strip_forall) clause 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/src/tfl/src/ |
| H A D | Defn.sml | 46 val (lhs,rhs) = dest_eq (snd(strip_forall hd_eqn)) value
51 let val (lhs,rhs) = dest_eq (snd (strip_forall (concl hd_eqn))) value
1101 val (lhs, rhs) = dest_eq (snd (strip_forall eq1)) value
[all...] |
| /seL4-l4v-10.1.1/HOL4/src/bool/ |
| H A D | boolScript.sml | 313 val lhs = fst o dest_eq; value
2157 val lhs = ���P \/ Q ==> R��� value
|
Completed in 104 milliseconds
1234