# HG changeset patch
# User wenzelm
# Date 1426848802 -3600
# Node ID df377a6fdd90c74218f086f6bd0420bf69ecd47d
# Parent  558acf0426f1fd367b34055f0e7773fffd7eec66
tuned;

diff -r 558acf0426f1 -r df377a6fdd90 src/HOL/Bali/AxExample.thy
--- a/src/HOL/Bali/AxExample.thy	Fri Mar 20 11:48:34 2015 +0100
+++ b/src/HOL/Bali/AxExample.thy	Fri Mar 20 11:53:22 2015 +0100
@@ -48,8 +48,8 @@
 
 fun ax_tac ctxt =
   REPEAT o rtac allI THEN'
-  resolve_tac ctxt (@{thm ax_Skip} :: @{thm ax_StatRef} :: @{thm ax_MethdN} :: @{thm ax_Alloc} ::
-    @{thm ax_Alloc_Arr} :: @{thm ax_SXAlloc_Normal} :: @{thms ax_derivs.intros(8-)});
+  resolve_tac ctxt
+    @{thms ax_Skip ax_StatRef ax_MethdN ax_Alloc ax_Alloc_Arr ax_SXAlloc_Normal ax_derivs.intros(8-)};
 *}