| changeset 58963 | 26bf09b95dda |
| parent 58889 | 5b7a9633cfa8 |
| child 63167 | 0909deb8059b |
--- a/src/HOL/NanoJava/Example.thy Sun Nov 09 20:49:28 2014 +0100 +++ b/src/HOL/NanoJava/Example.thy Mon Nov 10 21:49:48 2014 +0100 @@ -131,7 +131,7 @@ apply auto apply (case_tac "aa=a") apply auto -apply (tactic "smp_tac 1 1") +apply (tactic "smp_tac @{context} 1 1") apply (case_tac "aa=a") apply auto done