| changeset 69597 | ff784d5a5bfb |
| parent 68451 | c34aa23a1fb6 |
--- a/src/HOL/NanoJava/Example.thy Sat Jan 05 17:00:43 2019 +0100 +++ b/src/HOL/NanoJava/Example.thy Sat Jan 05 17:24:33 2019 +0100 @@ -131,7 +131,7 @@ apply auto apply (case_tac "aa=a") apply auto -apply (tactic "smp_tac @{context} 1 1") +apply (tactic "smp_tac \<^context> 1 1") apply (case_tac "aa=a") apply auto done