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 equality_name = "op =" |
|
20 val not_name = "Not" |
19 val notE = notE |
21 val notE = notE |
20 val ccontr = ccontr |
22 val ccontr = ccontr |
21 val contr_tac = Classical.contr_tac |
23 val contr_tac = Classical.contr_tac |
22 val dup_intr = Classical.dup_intr |
24 val dup_intr = Classical.dup_intr |
23 val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac |
25 val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac |