equal
deleted
inserted
replaced
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_cs = Classical.rep_cs |
78 val rep_cs = Classical.rep_cs |
79 val cla_method' = Classical.cla_method' |
79 val cla_modifiers = Classical.cla_modifiers; |
|
80 val cla_meth' = Classical.cla_meth' |
80 end; |
81 end; |
81 |
82 |
82 structure Blast = BlastFun(Blast_Data); |
83 structure Blast = BlastFun(Blast_Data); |
83 Blast.overloaded ("op =", domain_type); (*overloading of equality as iff*) |
84 Blast.overloaded ("op =", domain_type); (*overloading of equality as iff*) |
84 |
85 |