src/HOL/Isar_Examples/Expr_Compiler.thy

       by simp
     finally show ?case .
   next
     case (Load adr)
     from Cons show ?case
-      by simp -- \<open>same as above\<close>
+      by simp \<comment> \<open>same as above\<close>
   next
     case (Apply fn)
     have "exec ((Apply fn # xs) @ ys) s env =
         exec (Apply fn # xs @ ys) s env" by simp
     also have "\<dots> =

     also have "env adr = eval (Variable adr) env"
       by simp
     finally show ?case .
   next
     case (Constant val s)
-    show ?case by simp -- \<open>same as above\<close>
+    show ?case by simp \<comment> \<open>same as above\<close>
   next
     case (Binop fn e1 e2 s)
     have "exec (compile (Binop fn e1 e2)) s env =
         exec (compile e2 @ compile e1 @ [Apply fn]) s env"
       by simp