--- a/src/HOL/ROOT Sat Nov 14 12:55:05 2020 +0100 +++ b/src/HOL/ROOT Sat Nov 14 12:57:28 2020 +0100 @@ -959,6 +959,8 @@ VC_Principles Reference Complex_Types + document_theories + "HOL-SPARK-Examples.Greatest_Common_Divisor" document_files "complex_types.ads" "complex_types_app.adb"