equal
deleted
inserted
replaced
12 val imp_intr = impI |
12 val imp_intr = impI |
13 val rev_mp = rev_mp |
13 val rev_mp = rev_mp |
14 val subst = subst |
14 val subst = subst |
15 val sym = sym |
15 val sym = sym |
16 val thin_refl = prove_goal (the_context ()) |
16 val thin_refl = prove_goal (the_context ()) |
17 "!!X. [|x=x; PROP W|] ==> PROP W" (K [atac 1]); |
17 "!!X. [|x=x; PROP W|] ==> PROP W" (K [atac 1]); |
18 end; |
18 end; |
19 |
19 |
20 structure Hypsubst = HypsubstFun(Hypsubst_Data); |
20 structure Hypsubst = HypsubstFun(Hypsubst_Data); |
21 open Hypsubst; |
21 open Hypsubst; |
22 |
|
23 fun hyp_subst_tac' i thm = if i <= Thm.nprems_of thm andalso |
|
24 Term.exists_Const (fn ("op =", Type (_, [T, _])) => T <> Type ("o", []) | _ => false) |
|
25 (Library.nth_elem (i - 1, Thm.prems_of thm)) then hyp_subst_tac i thm else no_tac thm; |
|