Lines Matching defs:lhs
13 let val (lhs,rhs) = dest_eq t
14 val (lvar,LBody) = dest_exists lhs
28 let val (lhs,rhs) = dest_eq t
29 val (lvar,LBody) = dest_forall lhs
79 let val (lhs,rhs) = dest_eq t
80 val l1 = strip_disj lhs
90 let val (lhs,rhs) = dest_eq t
91 val l1 = strip_conj lhs
100 let val (lhs,rhs) = dest_eq t
101 val (la, lc) = dest_imp lhs;
112 let val (lhs,rhs) = dest_eq t
113 val (la, lc) = dest_imp lhs;
165 val (lhs, rhs) = dest_eq (concl thm)
168 SUBGOAL_THEN lhs ASSUME_MP_TAC THEN1 tac