src/FOL/blastdata.ML
author paulson
Fri, 05 Oct 2007 09:59:03 +0200
changeset 24854 0ebcd575d3c6
parent 21539 c5cf9243ad62
child 26287 df8e5362cff9
permissions -rw-r--r--
filtering out some package theorems


val ccontr = thm "ccontr";

(*** Applying BlastFun to create Blast_tac ***)
structure Blast_Data = 
  struct
  type claset	= Cla.claset
  val equality_name = "op ="
  val not_name = "Not"
  val notE	= notE
  val ccontr	= ccontr
  val contr_tac = Cla.contr_tac
  val dup_intr	= Cla.dup_intr
  val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
  val claset	= Cla.claset
  val rep_cs    = Cla.rep_cs
  val cla_modifiers = Cla.cla_modifiers;
  val cla_meth' = Cla.cla_meth'
  end;

structure Blast = BlastFun(Blast_Data);

val Blast_tac = Blast.Blast_tac
and blast_tac = Blast.blast_tac;