src/HOL/blastdata.ML
changeset 20944 34b2c1bb7178
parent 18524 57b489b54914
child 20973 0b8e436ed071
     1.1 --- a/src/HOL/blastdata.ML	Tue Oct 10 10:34:43 2006 +0200
     1.2 +++ b/src/HOL/blastdata.ML	Tue Oct 10 10:35:24 2006 +0200
     1.3 @@ -1,35 +1,29 @@
     1.4 +Classical.AddSEs [thm "alt_ex1E"];
     1.5  
     1.6 -(*Better then ex1E for classical reasoner: needs no quantifier duplication!*)
     1.7 -val major::prems = goal (the_context ())
     1.8 -    "[| ?! x. P(x);                                              \
     1.9 -\       !!x. [| P(x);  ALL y y'. P(y) & P(y') --> y=y' |] ==> R  \
    1.10 -\    |] ==> R";
    1.11 -by (rtac (major RS ex1E) 1);
    1.12 -by (REPEAT (ares_tac (allI::prems) 1));
    1.13 -by (etac (dup_elim allE) 1);
    1.14 -by (Fast_tac 1);
    1.15 -qed "alt_ex1E";
    1.16 -
    1.17 -AddSEs [alt_ex1E];
    1.18 -
    1.19 -(*** Applying BlastFun to create Blast_tac ***)
    1.20  structure Blast_Data = 
    1.21 -  struct
    1.22 -  type claset	= Classical.claset
    1.23 +struct
    1.24 +  type claset = Classical.claset
    1.25    val equality_name = "op ="
    1.26    val not_name = "Not"
    1.27 -  val notE	= notE
    1.28 -  val ccontr	= ccontr
    1.29 +  val notE = HOL.notE
    1.30 +  val ccontr = HOL.ccontr
    1.31    val contr_tac = Classical.contr_tac
    1.32 -  val dup_intr	= Classical.dup_intr
    1.33 +  val dup_intr = Classical.dup_intr
    1.34    val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
    1.35    val claset	= Classical.claset
    1.36 -  val rep_cs    = Classical.rep_cs
    1.37 -  val cla_modifiers = Classical.cla_modifiers;
    1.38 +  val rep_cs = Classical.rep_cs
    1.39 +  val cla_modifiers = Classical.cla_modifiers
    1.40    val cla_meth' = Classical.cla_meth'
    1.41 -  end;
    1.42 +end;
    1.43  
    1.44  structure Blast = BlastFun(Blast_Data);
    1.45  
    1.46 -val Blast_tac = Blast.Blast_tac
    1.47 -and blast_tac = Blast.blast_tac;
    1.48 +structure HOL =
    1.49 +struct
    1.50 +
    1.51 +open HOL;
    1.52 +
    1.53 +val Blast_tac = Blast.Blast_tac;
    1.54 +val blast_tac = Blast.blast_tac;
    1.55 +
    1.56 +end;
    1.57 \ No newline at end of file