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