changeset 77811 | ae9e6218443d |
parent 69605 | a96320074298 |
--- 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 \<open>Test infrastructure for the code generator\<close> + theory Code_Test imports Main keywords "test_code" :: diag