equal
deleted
inserted
replaced
41 declare lvar_def [simp] |
41 declare lvar_def [simp] |
42 |
42 |
43 ML {* |
43 ML {* |
44 fun inst1_tac ctxt s t xs st = |
44 fun inst1_tac ctxt s t xs st = |
45 (case AList.lookup (op =) (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 => Rule_Insts.instantiate_tac 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 rtac allI THEN' |
50 REPEAT o rtac allI THEN' |
51 resolve_tac ctxt (@{thm ax_Skip} :: @{thm ax_StatRef} :: @{thm ax_MethdN} :: @{thm ax_Alloc} :: |
51 resolve_tac ctxt (@{thm ax_Skip} :: @{thm ax_StatRef} :: @{thm ax_MethdN} :: @{thm ax_Alloc} :: |