0

1 
(** Generalized elimination rules **)


2 


3 
(*Generalized elimination for two conclusions*)

927

4 
val prems = goal proto_pure_thy

0

5 
"[ PROP U ==> PROP VA; \


6 
\ PROP U ==> PROP VB; \


7 
\ PROP U; \


8 
\ [ PROP VA; PROP VB ] ==> PROP W \


9 
\ ] ==> PROP W";


10 
by (REPEAT (resolve_tac prems 1));


11 
val general_elim2_rl = result();


12 


13 
fun make_elim2 (rl1,rl2) = standard (rl2 COMP rl1 COMP general_elim2_rl);


14 
fun elim2_tac (rl1,rl2) = eresolve_tac [rl2 COMP rl1 COMP general_elim2_rl];


15 


16 


17 
(*For example, make_elim2(conjunct1,conjunct2)


18 
yields conjunction elimination *)
