author | wenzelm |
Wed, 14 Feb 2001 23:18:47 +0100 | |
changeset 11125 | b70c3c1b499f |
parent 10906 | de95ba2760fe |
child 11748 | 06eb315831ff |
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 atomize = atomize_rules 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;