src/HOL/blastdata.ML
author paulson
Tue Jun 28 15:27:45 2005 +0200 (2005-06-28)
changeset 16587 b34c8aa657a5
parent 13550 5a176b8dda84
child 16774 515b6020cf5d
permissions -rw-r--r--
Constant "If" is now local
     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
    26   val cla_modifiers = Classical.cla_modifiers;
    27   val cla_meth' = Classical.cla_meth'
    28   end;
    29 
    30 structure Blast = BlastFun(Blast_Data);
    31 
    32 val Blast_tac = Blast.Blast_tac
    33 and blast_tac = Blast.blast_tac;