changeset 74101 | d804e93ae9ff |
parent 73932 | fd21b4a93043 |
child 74424 | 2cf4d6cf4c0d |
--- a/src/HOL/List.thy Sun Aug 01 23:18:13 2021 +0200 +++ b/src/HOL/List.thy Mon Aug 02 10:01:06 2021 +0000 @@ -5,7 +5,7 @@ section \<open>The datatype of finite lists\<close> theory List -imports Sledgehammer Code_Numeral Lifting_Set +imports Sledgehammer Lifting_Set begin datatype (set: 'a) list =