|
7355
|
1 |
|
|
|
2 |
(*** Applying BlastFun to create Blast_tac ***)
|
|
|
3 |
structure Blast_Data =
|
|
|
4 |
struct
|
|
|
5 |
type claset = Cla.claset
|
|
|
6 |
val notE = notE
|
|
|
7 |
val ccontr = ccontr
|
|
|
8 |
val contr_tac = Cla.contr_tac
|
|
|
9 |
val dup_intr = Cla.dup_intr
|
|
|
10 |
val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
|
|
|
11 |
val claset = Cla.claset
|
|
|
12 |
val rep_cs = Cla.rep_cs
|
|
10429
|
13 |
val atomize = thms "atomize'"
|
|
7355
|
14 |
val cla_modifiers = Cla.cla_modifiers;
|
|
|
15 |
val cla_meth' = Cla.cla_meth'
|
|
|
16 |
end;
|
|
|
17 |
|
|
|
18 |
structure Blast = BlastFun(Blast_Data);
|
|
|
19 |
|
|
|
20 |
val Blast_tac = Blast.Blast_tac
|
|
|
21 |
and blast_tac = Blast.blast_tac;
|