src/FOL/blastdata.ML
changeset 18171 c4f873d65603
parent 16774 515b6020cf5d
child 18524 57b489b54914
equal deleted inserted replaced
18170:73ce773f12de 18171:c4f873d65603
     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
       
     7   val notE	= notE
     6   val notE	= notE
     8   val ccontr	= ccontr
     7   val ccontr	= ccontr
     9   val contr_tac = Cla.contr_tac
     8   val contr_tac = Cla.contr_tac
    10   val dup_intr	= Cla.dup_intr
     9   val dup_intr	= Cla.dup_intr
    11   val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
    10   val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac