author | paulson |
Tue, 12 Jul 2005 12:49:46 +0200 | |
changeset 16774 | 515b6020cf5d |
parent 11748 | 06eb315831ff |
child 18171 | c4f873d65603 |
permissions | -rw-r--r-- |
(*** Applying BlastFun to create Blast_tac ***) structure Blast_Data = struct type claset = Cla.claset val is_hol = false 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;