equal
deleted
inserted
replaced
274 (* |
274 (* |
275 inductive premises can be of the form |
275 inductive premises can be of the form |
276 R ... /\ P ...; split_conj_i picks out |
276 R ... /\ P ...; split_conj_i picks out |
277 the part R or P part |
277 the part R or P part |
278 *) |
278 *) |
279 fun split_conj1 names (Const ("op &", _) $ f1 $ f2) = |
279 fun split_conj1 names (Const (@{const_name "op &"}, _) $ f1 $ f2) = |
280 (case head_of f1 of |
280 (case head_of f1 of |
281 Const (name, _) => if member (op =) names name then SOME f1 else NONE |
281 Const (name, _) => if member (op =) names name then SOME f1 else NONE |
282 | _ => NONE) |
282 | _ => NONE) |
283 | split_conj1 _ _ = NONE; |
283 | split_conj1 _ _ = NONE; |
284 |
284 |
285 fun split_conj2 names (Const ("op &", _) $ f1 $ f2) = |
285 fun split_conj2 names (Const (@{const_name "op &"}, _) $ f1 $ f2) = |
286 (case head_of f1 of |
286 (case head_of f1 of |
287 Const (name, _) => if member (op =) names name then SOME f2 else NONE |
287 Const (name, _) => if member (op =) names name then SOME f2 else NONE |
288 | _ => NONE) |
288 | _ => NONE) |
289 | split_conj2 _ _ = NONE; |
289 | split_conj2 _ _ = NONE; |
290 |
290 |