src/HOL/blastdata.ML
author haftmann
Mon Aug 14 13:46:06 2006 +0200 (2006-08-14)
changeset 20380 14f9f2a1caa6
parent 18524 57b489b54914
child 20944 34b2c1bb7178
permissions -rw-r--r--
simplified code generator setup
     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 equality_name = "op ="
    20   val not_name = "Not"
    21   val notE	= notE
    22   val ccontr	= ccontr
    23   val contr_tac = Classical.contr_tac
    24   val dup_intr	= Classical.dup_intr
    25   val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
    26   val claset	= Classical.claset
    27   val rep_cs    = Classical.rep_cs
    28   val cla_modifiers = Classical.cla_modifiers;
    29   val cla_meth' = Classical.cla_meth'
    30   end;
    31 
    32 structure Blast = BlastFun(Blast_Data);
    33 
    34 val Blast_tac = Blast.Blast_tac
    35 and blast_tac = Blast.blast_tac;