src/FOL/ex/Miniscope.thy
changeset 58838 59203adfc33f
parent 51717 9e7d1c139569
child 59498 50b60f501b05
     1.1 --- a/src/FOL/ex/Miniscope.thy	Thu Oct 30 16:20:46 2014 +0100
     1.2 +++ b/src/FOL/ex/Miniscope.thy	Thu Oct 30 16:55:29 2014 +0100
     1.3 @@ -65,7 +65,7 @@
     1.4  
     1.5  ML {*
     1.6  val mini_ss = simpset_of (@{context} addsimps @{thms mini_simps});
     1.7 -fun mini_tac ctxt = rtac @{thm ccontr} THEN' asm_full_simp_tac (put_simpset mini_ss ctxt);
     1.8 +fun mini_tac ctxt = resolve_tac @{thms ccontr} THEN' asm_full_simp_tac (put_simpset mini_ss ctxt);
     1.9  *}
    1.10  
    1.11  end