Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned proof;
authorwenzelm
Tue, 24 Mar 2015 16:16:48 +0100
changeset 59797 f313ca9fbba0
parent 59796 f05ef8c62e4f
child 59798 45c89526208f
tuned proof;
src/HOL/HOLCF/Compact_Basis.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/HOLCF/Compact_Basis.thy	Tue Mar 24 15:57:51 2015 +0100
+++ b/src/HOL/HOLCF/Compact_Basis.thy	Tue Mar 24 16:16:48 2015 +0100
@@ -16,7 +16,7 @@
 
 typedef 'a pd_basis = "pd_basis :: 'a compact_basis set set"
   unfolding pd_basis_def
-  apply (rule_tac x="{a}" for a in exI)
+  apply (rule_tac x="{_}" in exI)
   apply simp
   done
isabelle