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
Mon, 23 Mar 2015 23:12:33 +0100
changeset 59791 d9765e17947f
parent 59790 85c572d089fc
child 59792 f19f4afa49e2
tuned proof;
src/HOL/HOLCF/Compact_Basis.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/HOLCF/Compact_Basis.thy	Mon Mar 23 22:57:04 2015 +0100
+++ b/src/HOL/HOLCF/Compact_Basis.thy	Mon Mar 23 23:12:33 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="{arbitrary}" in exI)
+  apply (rule_tac x="{a}" for a in exI)
   apply simp
   done
isabelle