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