author | wenzelm |
Tue, 01 Aug 2000 11:58:14 +0200 | |
changeset 9487 | 7e377f912629 |
parent 9486 | 2df511ebb956 |
child 9561 | 714ad541a133 |
permissions | -rw-r--r-- |
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 |
|
9486
2df511ebb956
handle actual object-logic rules by atomizing the goal;
wenzelm
parents:
7355
diff
changeset
|
13 |
val atomize = [thm "all_eq", thm "imp_eq"] |
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; |