| author | wenzelm |
| Wed, 15 Apr 2009 11:14:48 +0200 | |
| changeset 30895 | bad26d8f0adf |
| parent 30609 | 983e8b6e4e69 |
| permissions | -rw-r--r-- |
| 7355 | 1 |
|
|
30609
983e8b6e4e69
Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
wenzelm
parents:
26287
diff
changeset
|
2 |
(*** Applying BlastFun to create blast_tac ***) |
| 7355 | 3 |
structure Blast_Data = |
4 |
struct |
|
5 |
type claset = Cla.claset |
|
| 26287 | 6 |
val equality_name = @{const_name "op ="}
|
7 |
val not_name = @{const_name Not}
|
|
8 |
val notE = @{thm notE}
|
|
9 |
val ccontr = @{thm ccontr}
|
|
| 7355 | 10 |
val contr_tac = Cla.contr_tac |
11 |
val dup_intr = Cla.dup_intr |
|
12 |
val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac |
|
|
30609
983e8b6e4e69
Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
wenzelm
parents:
26287
diff
changeset
|
13 |
val rep_cs = Cla.rep_cs |
| 7355 | 14 |
val cla_modifiers = Cla.cla_modifiers; |
15 |
val cla_meth' = Cla.cla_meth' |
|
16 |
end; |
|
17 |
||
18 |
structure Blast = BlastFun(Blast_Data); |
|
|
30609
983e8b6e4e69
Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
wenzelm
parents:
26287
diff
changeset
|
19 |
val blast_tac = Blast.blast_tac; |