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/HOLCF/CompactBasis.thy
changeset 29244 95d591908d8d
parent 29237 e90d9d51106b
child 29252 ea97aa6aeba2 
--- a/src/HOLCF/CompactBasis.thy	Fri Dec 19 11:09:31 2008 +0100
+++ b/src/HOLCF/CompactBasis.thy	Fri Dec 19 11:57:21 2008 +0100
@@ -244,7 +244,7 @@
   assumes "ab_semigroup_idem_mult f"
   shows "fold_pd g f (PDPlus t u) = f (fold_pd g f t) (fold_pd g f u)"
 proof -
-  interpret ab_semigroup_idem_mult f by fact
+  class_interpret ab_semigroup_idem_mult [f] by fact
   show ?thesis unfolding fold_pd_def Rep_PDPlus by (simp add: image_Un fold1_Un2)
 qed
isabelle