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/HOLCF/UpperPD.thy
changeset 67682 00c436488398
parent 62175 8ffc4d0e652d 
--- a/src/HOL/HOLCF/UpperPD.thy	Tue Feb 20 22:04:04 2018 +0100
+++ b/src/HOL/HOLCF/UpperPD.thy	Tue Feb 20 22:25:23 2018 +0100
@@ -416,8 +416,8 @@
   assumes "finite_deflation d" shows "finite_deflation (upper_map\<cdot>d)"
 proof (rule finite_deflation_intro)
   interpret d: finite_deflation d by fact
-  have "deflation d" by fact
-  thus "deflation (upper_map\<cdot>d)" by (rule deflation_upper_map)
+  from d.deflation_axioms show "deflation (upper_map\<cdot>d)"
+    by (rule deflation_upper_map)
   have "finite (range (\<lambda>x. d\<cdot>x))" by (rule d.finite_range)
   hence "finite (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x))"
     by (rule finite_vimageI, simp add: inj_on_def Rep_compact_basis_inject)
isabelle