| changeset 60754 | 02924903a6fd |
| parent 59807 | 22bc39064290 |
| child 62042 | 6c6ccf573479 |
--- a/src/HOL/Bali/AxExample.thy Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/Bali/AxExample.thy Sat Jul 18 20:54:56 2015 +0200 @@ -47,7 +47,7 @@ | NONE => Seq.empty); fun ax_tac ctxt = - REPEAT o rtac allI THEN' + REPEAT o resolve_tac ctxt [allI] THEN' resolve_tac ctxt @{thms ax_Skip ax_StatRef ax_MethdN ax_Alloc ax_Alloc_Arr ax_SXAlloc_Normal ax_derivs.intros(8-)}; *}