equal
deleted
inserted
replaced
21 val contr_tac = Classical.contr_tac |
21 val contr_tac = Classical.contr_tac |
22 val dup_intr = Classical.dup_intr |
22 val dup_intr = Classical.dup_intr |
23 val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac |
23 val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac |
24 val claset = Classical.claset |
24 val claset = Classical.claset |
25 val rep_cs = Classical.rep_cs |
25 val rep_cs = Classical.rep_cs |
|
26 val atomize = [thm "all_eq", thm "imp_eq"] |
26 val cla_modifiers = Classical.cla_modifiers; |
27 val cla_modifiers = Classical.cla_modifiers; |
27 val cla_meth' = Classical.cla_meth' |
28 val cla_meth' = Classical.cla_meth' |
28 end; |
29 end; |
29 |
30 |
30 structure Blast = BlastFun(Blast_Data); |
31 structure Blast = BlastFun(Blast_Data); |