equal
deleted
inserted
replaced
40 declare if_split_asm [split del] |
40 declare if_split_asm [split del] |
41 declare lvar_def [simp] |
41 declare lvar_def [simp] |
42 |
42 |
43 ML \<open> |
43 ML \<open> |
44 fun inst1_tac ctxt s t xs st = |
44 fun inst1_tac ctxt s t xs st = |
45 (case AList.lookup (=) (rev (Term.add_var_names (Thm.prop_of st) [])) s of |
45 (case AList.lookup (op =) (rev (Term.add_var_names (Thm.prop_of st) [])) s of |
46 SOME i => PRIMITIVE (Rule_Insts.read_instantiate ctxt [(((s, i), Position.none), t)] xs) st |
46 SOME i => PRIMITIVE (Rule_Insts.read_instantiate ctxt [(((s, i), Position.none), t)] xs) st |
47 | NONE => Seq.empty); |
47 | NONE => Seq.empty); |
48 |
48 |
49 fun ax_tac ctxt = |
49 fun ax_tac ctxt = |
50 REPEAT o resolve_tac ctxt [allI] THEN' |
50 REPEAT o resolve_tac ctxt [allI] THEN' |