diff -r 1a9decb8bfbc -r ae9e6218443d src/HOL/Library/Code_Cardinality.thy --- a/src/HOL/Library/Code_Cardinality.thy Mon Apr 10 23:21:47 2023 +0200 +++ b/src/HOL/Library/Code_Cardinality.thy Tue Apr 11 11:59:02 2023 +0000 @@ -1,4 +1,4 @@ -subsection \Code setup for sets with cardinality type information\ +section \Code setup for sets with cardinality type information\ theory Code_Cardinality imports Cardinality begin