9 Needs explicit instantiation of assumptions? |
9 Needs explicit instantiation of assumptions? |
10 |
10 |
11 |
11 |
12 Blast_tac is often more powerful than fast_tac, but has some limitations. |
12 Blast_tac is often more powerful than fast_tac, but has some limitations. |
13 Blast_tac... |
13 Blast_tac... |
14 * ignores addss, addbefore, addafter; this restriction is intrinsic |
14 * ignores wrappers (addss, addbefore, addafter, addWrapper, ...); |
|
15 this restriction is intrinsic |
15 * ignores elimination rules that don't have the correct format |
16 * ignores elimination rules that don't have the correct format |
16 (conclusion must be a formula variable) |
17 (conclusion must be a formula variable) |
17 * ignores types, which can make HOL proofs fail |
18 * ignores types, which can make HOL proofs fail |
18 * rules must not require higher-order unification, e.g. apply_type in ZF |
19 * rules must not require higher-order unification, e.g. apply_type in ZF |
19 + message "Function Var's argument not a bound variable" relates to this |
20 + message "Function Var's argument not a bound variable" relates to this |
58 val ccontr : thm |
59 val ccontr : thm |
59 val contr_tac : int -> tactic |
60 val contr_tac : int -> tactic |
60 val dup_intr : thm -> thm |
61 val dup_intr : thm -> thm |
61 val hyp_subst_tac : bool ref -> int -> tactic |
62 val hyp_subst_tac : bool ref -> int -> tactic |
62 val claset : unit -> claset |
63 val claset : unit -> claset |
63 val rep_claset : |
64 val rep_claset : (* dependent on classical.ML *) |
64 claset -> {safeIs: thm list, safeEs: thm list, |
65 claset -> {safeIs: thm list, safeEs: thm list, |
65 hazIs: thm list, hazEs: thm list, |
66 hazIs: thm list, hazEs: thm list, |
66 uwrapper: (int -> tactic) -> (int -> tactic), |
67 swrappers: (string * wrapper) list, |
67 swrapper: (int -> tactic) -> (int -> tactic), |
68 uwrappers: (string * wrapper) list, |
68 safe0_netpair: netpair, safep_netpair: netpair, |
69 safe0_netpair: netpair, safep_netpair: netpair, |
69 haz_netpair: netpair, dup_netpair: netpair} |
70 haz_netpair: netpair, dup_netpair: netpair} |
70 end; |
71 end; |
71 |
72 |
72 |
73 |