tuned proof;
authorwenzelm
Mon Mar 23 23:12:33 2015 +0100 (2015-03-23)
changeset 59791d9765e17947f
parent 59790 85c572d089fc
child 59792 f19f4afa49e2
tuned proof;
src/HOL/HOLCF/Compact_Basis.thy
     1.1 --- a/src/HOL/HOLCF/Compact_Basis.thy	Mon Mar 23 22:57:04 2015 +0100
     1.2 +++ b/src/HOL/HOLCF/Compact_Basis.thy	Mon Mar 23 23:12:33 2015 +0100
     1.3 @@ -16,7 +16,7 @@
     1.4  
     1.5  typedef 'a pd_basis = "pd_basis :: 'a compact_basis set set"
     1.6    unfolding pd_basis_def
     1.7 -  apply (rule_tac x="{arbitrary}" in exI)
     1.8 +  apply (rule_tac x="{a}" for a in exI)
     1.9    apply simp
    1.10    done
    1.11