equal
deleted
inserted
replaced
59 ("claset", ThyMethods {merge = merge, put = put, get = get}) |
59 ("claset", ThyMethods {merge = merge, put = put, get = get}) |
60 end; |
60 end; |
61 |
61 |
62 claset := HOL_cs; |
62 claset := HOL_cs; |
63 |
63 |
|
64 |
|
65 (*** Applying BlastFun to create Blast_tac ***) |
|
66 structure Blast_Data = |
|
67 struct |
|
68 type claset = Classical.claset |
|
69 val notE = notE |
|
70 val ccontr = ccontr |
|
71 val contr_tac = Classical.contr_tac |
|
72 val dup_intr = Classical.dup_intr |
|
73 val vars_gen_hyp_subst_tac = Hypsubst.vars_gen_hyp_subst_tac |
|
74 val claset = Classical.claset |
|
75 val rep_claset = Classical.rep_claset |
|
76 end; |
|
77 |
|
78 structure Blast = BlastFun(Blast_Data); |
|
79 |
|
80 val Blast_tac = Blast.Blast_tac |
|
81 and blast_tac = Blast.blast_tac; |