diff -r 1a9decb8bfbc -r ae9e6218443d src/HOL/Library/Code_Test.thy --- a/src/HOL/Library/Code_Test.thy Mon Apr 10 23:21:47 2023 +0200 +++ b/src/HOL/Library/Code_Test.thy Tue Apr 11 11:59:02 2023 +0000 @@ -4,6 +4,8 @@ Test infrastructure for the code generator. *) +section \Test infrastructure for the code generator\ + theory Code_Test imports Main keywords "test_code" :: diag