author | paulson |
Fri, 29 Oct 2004 15:16:02 +0200 | |
changeset 15270 | 8b3f707a78a7 |
parent 11748 | 06eb315831ff |
child 16774 | 515b6020cf5d |
permissions | -rw-r--r-- |
(*** Applying BlastFun to create Blast_tac ***) structure Blast_Data = struct type claset = Cla.claset 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;