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