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/Pcpodef.thy
changeset 25925 3dc4acca4388
parent 25921 0ca392ab7f37
child 25926 aa0eca1ccb19 
--- a/src/HOLCF/Pcpodef.thy	Fri Jan 18 08:30:12 2008 +0100
+++ b/src/HOLCF/Pcpodef.thy	Fri Jan 18 20:22:07 2008 +0100
@@ -104,7 +104,7 @@
     and adm:  "adm (\<lambda>x. x \<in> A)"
   shows "chain S \<Longrightarrow> Rep (Abs (\<Squnion>i. Rep (S i))) = (\<Squnion>i. Rep (S i))"
  apply (rule type_definition.Abs_inverse [OF type])
- apply (erule admD [OF adm ch2ch_Rep [OF less], rule_format])
+ apply (erule admD [OF adm ch2ch_Rep [OF less]])
  apply (rule type_definition.Rep [OF type])
 done
isabelle