src/HOL/Enum.thy
changeset 65956 639eb3617a86
parent 64592 7759f1766189
child 66806 a4e82b58d833
     1.1 --- a/src/HOL/Enum.thy	Sun May 28 15:46:26 2017 +0200
     1.2 +++ b/src/HOL/Enum.thy	Mon May 29 09:14:15 2017 +0200
     1.3 @@ -385,7 +385,7 @@
     1.4  begin
     1.5  
     1.6  definition
     1.7 -  "enum = map set (sublists enum)"
     1.8 +  "enum = map set (subseqs enum)"
     1.9  
    1.10  definition
    1.11    "enum_all P \<longleftrightarrow> (\<forall>A\<in>set enum. P (A::'a set))"
    1.12 @@ -394,7 +394,7 @@
    1.13    "enum_ex P \<longleftrightarrow> (\<exists>A\<in>set enum. P (A::'a set))"
    1.14  
    1.15  instance proof
    1.16 -qed (simp_all add: enum_set_def enum_all_set_def enum_ex_set_def sublists_powset distinct_set_sublists
    1.17 +qed (simp_all add: enum_set_def enum_all_set_def enum_ex_set_def subseqs_powset distinct_set_subseqs
    1.18    enum_distinct enum_UNIV)
    1.19  
    1.20  end