equal
deleted
inserted
replaced
73 val ccontr = ccontr |
73 val ccontr = ccontr |
74 val contr_tac = Classical.contr_tac |
74 val contr_tac = Classical.contr_tac |
75 val dup_intr = Classical.dup_intr |
75 val dup_intr = Classical.dup_intr |
76 val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac |
76 val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac |
77 val claset = Classical.claset |
77 val claset = Classical.claset |
78 val rep_claset = Classical.rep_claset |
78 val rep_cs = Classical.rep_cs |
79 end; |
79 end; |
80 |
80 |
81 structure Blast = BlastFun(Blast_Data); |
81 structure Blast = BlastFun(Blast_Data); |
82 Blast.overloaded ("op =", domain_type); (*overloading of equality as iff*) |
82 Blast.overloaded ("op =", domain_type); (*overloading of equality as iff*) |
83 |
83 |