adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

lib: avoid @{file} for files that might be moved 

The theory Value_Types is used without Value_Types_Test in the
AutoCorres release, which makes the @{file ..} antiquotation fail.
Including Value_Types_Test in the dependencies of Value_Types to
include it in the release doesn't work, because that would be a
circular dependency.

So to avoid manually enumerating release files, we make this a pure
@{text ..} antiquotation instead.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein 2022-10-31 11:28:43 +11:00 committed by Gerwin Klein
parent 91c135d440
commit 013115dcde
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
lib/Value_Type.thy
View File

@ -18,7 +18,7 @@ begin
value_type num_something = "10 * num_domains"
*)
text \<open>See theory @{file "test/Value_Type_Test.thy"} for further example/demo.\<close>
text \<open>See theory @{text "test/Value_Type_Test.thy"} for further example/demo.\<close>
ML \<open>