equal
deleted
inserted
replaced
477 Goal.prove ctxt [] [] goal (fn _ => map_thm_tac ctxt tac thm) |
477 Goal.prove ctxt [] [] goal (fn _ => map_thm_tac ctxt tac thm) |
478 end |
478 end |
479 |
479 |
480 (* |
480 (* |
481 inductive premises can be of the form |
481 inductive premises can be of the form |
482 R ... /\ P ...; split_conj_i picks out |
482 |
483 the part R or P part |
483 R ... /\ P ...; |
|
484 |
|
485 split_conj_i picks out the part R or P part |
484 *) |
486 *) |
485 fun split_conj1 names (Const (@{const_name "conj"}, _) $ f1 $ _) = |
487 fun split_conj1 names (Const (@{const_name "conj"}, _) $ f1 $ _) = |
486 (case head_of f1 of |
488 (case head_of f1 of |
487 Const (name, _) => if member (op =) names name then SOME f1 else NONE |
489 Const (name, _) => if member (op =) names name then SOME f1 else NONE |
488 | _ => NONE) |
490 | _ => NONE) |