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/Metis_Examples/Message.thy
changeset 69712 dc85b5b3a532
parent 69597 ff784d5a5bfb
child 76339 9e1fef7b4f29 
--- a/src/HOL/Metis_Examples/Message.thy	Tue Jan 22 10:50:47 2019 +0000
+++ b/src/HOL/Metis_Examples/Message.thy	Tue Jan 22 12:00:16 2019 +0000
@@ -78,7 +78,7 @@
 lemma parts_mono: "G \<subseteq> H ==> parts(G) \<subseteq> parts(H)"
 apply auto
 apply (erule parts.induct)
-   apply (metis parts.Inj set_rev_mp)
+   apply (metis parts.Inj rev_subsetD)
   apply (metis parts.Fst)
  apply (metis parts.Snd)
 by (metis parts.Body)
isabelle