src/HOL/Enum.thy
changeset 61799 4cf66f21b764
parent 61169 4de9ff3ea29a
child 62343 24106dc44def
     1.1 --- a/src/HOL/Enum.thy	Mon Dec 07 10:23:50 2015 +0100
     1.2 +++ b/src/HOL/Enum.thy	Mon Dec 07 10:38:04 2015 +0100
     1.3 @@ -6,7 +6,7 @@
     1.4  imports Map Groups_List
     1.5  begin
     1.6  
     1.7 -subsection \<open>Class @{text enum}\<close>
     1.8 +subsection \<open>Class \<open>enum\<close>\<close>
     1.9  
    1.10  class enum =
    1.11    fixes enum :: "'a list"
    1.12 @@ -16,7 +16,7 @@
    1.13      and enum_distinct: "distinct enum"
    1.14    assumes enum_all_UNIV: "enum_all P \<longleftrightarrow> Ball UNIV P"
    1.15    assumes enum_ex_UNIV: "enum_ex P \<longleftrightarrow> Bex UNIV P" 
    1.16 -   -- \<open>tailored towards simple instantiation\<close>
    1.17 +   \<comment> \<open>tailored towards simple instantiation\<close>
    1.18  begin
    1.19  
    1.20  subclass finite proof