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