src/HOL/Library/FinFun.thy
changeset 60583 a645a0e6d790
parent 60565 b7ee41f72add
child 61384 9f5145281888
     1.1 --- a/src/HOL/Library/FinFun.thy	Thu Jun 25 23:51:54 2015 +0200
     1.2 +++ b/src/HOL/Library/FinFun.thy	Fri Jun 26 00:14:10 2015 +0200
     1.3 @@ -1320,11 +1320,10 @@
     1.4  lemma set_finfun_to_list [simp]: "set (finfun_to_list f) = {x. finfun_dom f $ x}" (is ?thesis1)
     1.5    and sorted_finfun_to_list: "sorted (finfun_to_list f)" (is ?thesis2)
     1.6    and distinct_finfun_to_list: "distinct (finfun_to_list f)" (is ?thesis3)
     1.7 -proof -
     1.8 -  have "?thesis1 \<and> ?thesis2 \<and> ?thesis3"
     1.9 +proof (atomize (full))
    1.10 +  show "?thesis1 \<and> ?thesis2 \<and> ?thesis3"
    1.11      unfolding finfun_to_list_def
    1.12      by(rule theI')(rule finite_sorted_distinct_unique finite_finfun_dom)+
    1.13 -  thus ?thesis1 ?thesis2 ?thesis3 by simp_all
    1.14  qed
    1.15  
    1.16  lemma finfun_const_False_conv_bot: "op $ (K$ False) = bot"