7357

1 


2 
(*Better then ex1E for classical reasoner: needs no quantifier duplication!*)


3 
val major::prems = goal (the_context ())


4 
"[ ?! x. P(x); \


5 
\ !!x. [ P(x); ALL y y'. P(y) & P(y') > y=y' ] ==> R \


6 
\ ] ==> R";


7 
by (rtac (major RS ex1E) 1);


8 
by (REPEAT (ares_tac (allI::prems) 1));


9 
by (etac (dup_elim allE) 1);


10 
by (Fast_tac 1);


11 
qed "alt_ex1E";


12 


13 
AddSEs [alt_ex1E];


14 


15 
(*** Applying BlastFun to create Blast_tac ***)


16 
structure Blast_Data =


17 
struct


18 
type claset = Classical.claset


19 
val notE = notE


20 
val ccontr = ccontr


21 
val contr_tac = Classical.contr_tac


22 
val dup_intr = Classical.dup_intr


23 
val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac


24 
val claset = Classical.claset


25 
val rep_cs = Classical.rep_cs

10429

26 
val atomize = thms "atomize'"

7357

27 
val cla_modifiers = Classical.cla_modifiers;


28 
val cla_meth' = Classical.cla_meth'


29 
end;


30 


31 
structure Blast = BlastFun(Blast_Data);


32 
Blast.overloaded ("op =", domain_type); (*overloading of equality as iff*)


33 


34 
val Blast_tac = Blast.Blast_tac


35 
and blast_tac = Blast.blast_tac;
