changeset 60754 | 02924903a6fd |
parent 59378 | 065f349852e6 |
child 61337 | 4645502c3c64 |
--- a/src/Doc/Codegen/Evaluation.thy Sat Jul 18 20:53:05 2015 +0200 +++ b/src/Doc/Codegen/Evaluation.thy Sat Jul 18 20:54:56 2015 +0200 @@ -232,7 +232,7 @@ ML_prf (*>*) \<open>val thm = Reification.conv @{context} @{thms interp.simps} @{cterm "x < y \<and> x < z"}\<close> (*<*) -by (tactic \<open>ALLGOALS (rtac thm)\<close>) +by (tactic \<open>ALLGOALS (resolve_tac @{context} [thm])\<close>) (*>*) text \<open>