equal
deleted
inserted
replaced
14 |
14 |
15 (*** Applying BlastFun to create Blast_tac ***) |
15 (*** Applying BlastFun to create Blast_tac ***) |
16 structure Blast_Data = |
16 structure Blast_Data = |
17 struct |
17 struct |
18 type claset = Classical.claset |
18 type claset = Classical.claset |
|
19 val is_hol = true |
19 val notE = notE |
20 val notE = notE |
20 val ccontr = ccontr |
21 val ccontr = ccontr |
21 val contr_tac = Classical.contr_tac |
22 val contr_tac = Classical.contr_tac |
22 val dup_intr = Classical.dup_intr |
23 val dup_intr = Classical.dup_intr |
23 val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac |
24 val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac |