| changeset 14174 | f3cafd2929d5 |
| parent 14144 | 7195c9b0423f |
| child 16417 | 9bc16273c2d4 |
--- a/src/HOL/MicroJava/J/State.thy Fri Aug 29 13:18:45 2003 +0200 +++ b/src/HOL/MicroJava/J/State.thy Fri Aug 29 15:19:02 2003 +0200 @@ -73,7 +73,7 @@ apply(simp add: Pair_fst_snd_eq Eps_split) apply(rule someI) apply(rule disjI2) -apply(rule_tac "r" = "snd (?a,Some (Addr (XcptRef OutOfMemory)))" in trans) +apply(rule_tac r = "snd (?a,Some (Addr (XcptRef OutOfMemory)))" in trans) apply auto done