Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/MicroJava/J/Example.thy
changeset 61424 c3658c18b7bc
parent 61361 8b5f00202e1a
child 62042 6c6ccf573479 
--- a/src/HOL/MicroJava/J/Example.thy	Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/MicroJava/J/Example.thy	Tue Oct 13 09:21:15 2015 +0200
@@ -434,7 +434,7 @@
 apply     (simp (no_asm))
 apply     (rule e) -- "XcptE"
 apply    (simp (no_asm))
-apply   (rule surjective_pairing [symmetric, THEN[2]trans], subst Pair_eq, force)
+apply   (rule surjective_pairing [symmetric, THEN[2]trans], subst prod.inject, force)
 apply  (simp (no_asm))
 apply (simp (no_asm))
 apply (rule e) -- "XcptE"
isabelle