src/HOL/Bali/AxSem.thy
changeset 26342 0f65fa163304
parent 24783 5a3e336a2e37
child 26480 544cef16045b
     1.1 --- a/src/HOL/Bali/AxSem.thy	Wed Mar 19 22:47:39 2008 +0100
     1.2 +++ b/src/HOL/Bali/AxSem.thy	Wed Mar 19 22:50:42 2008 +0100
     1.3 @@ -699,7 +699,7 @@
     1.4  (*42 subgoals*)
     1.5  apply       (tactic "ALLGOALS strip_tac")
     1.6  apply       (tactic {* ALLGOALS(REPEAT o (EVERY'[dtac (thm "subset_singletonD"),
     1.7 -         etac disjE, fast_tac (claset() addSIs [thm "ax_derivs.empty"])]))*})
     1.8 +         etac disjE, fast_tac (@{claset} addSIs [thm "ax_derivs.empty"])]))*})
     1.9  apply       (tactic "TRYALL hyp_subst_tac")
    1.10  apply       (simp, rule ax_derivs.empty)
    1.11  apply      (drule subset_insertD)