src/FOL/blastdata.ML
changeset 16774 515b6020cf5d
parent 11748 06eb315831ff
child 18171 c4f873d65603
equal deleted inserted replaced
16773:33c4d8fe6f78 16774:515b6020cf5d
     1 
     1 
     2 (*** Applying BlastFun to create Blast_tac ***)
     2 (*** Applying BlastFun to create Blast_tac ***)
     3 structure Blast_Data = 
     3 structure Blast_Data = 
     4   struct
     4   struct
     5   type claset	= Cla.claset
     5   type claset	= Cla.claset
       
     6   val is_hol    = false
     6   val notE	= notE
     7   val notE	= notE
     7   val ccontr	= ccontr
     8   val ccontr	= ccontr
     8   val contr_tac = Cla.contr_tac
     9   val contr_tac = Cla.contr_tac
     9   val dup_intr	= Cla.dup_intr
    10   val dup_intr	= Cla.dup_intr
    10   val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
    11   val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac