changeset 59199 | cb8e5f7a5e4a |
parent 58886 | 8a6cac7c7247 |
child 59498 | 50b60f501b05 |
--- a/src/HOL/MicroJava/J/Example.thy Mon Dec 29 20:51:42 2014 +0100 +++ b/src/HOL/MicroJava/J/Example.thy Mon Dec 29 21:02:49 2014 +0100 @@ -434,7 +434,7 @@ apply (simp (no_asm)) apply (tactic e) -- "XcptE" apply (simp (no_asm)) -apply (rule surjective_pairing [THEN sym, THEN[2]trans], subst Pair_eq, force) +apply (rule surjective_pairing [symmetric, THEN[2]trans], subst Pair_eq, force) apply (simp (no_asm)) apply (simp (no_asm)) apply (tactic e) -- "XcptE"