diff --git a/Citadelle/examples/C_Model_init.thy b/Citadelle/examples/C_Model_init.thy index b39139d1cd9a64878c4e6e33e28226d70e2e44a3..8282218d883be5affd69514fde67db5907cbc7bb 100644 --- a/Citadelle/examples/C_Model_init.thy +++ b/Citadelle/examples/C_Model_init.thy @@ -38,7 +38,7 @@ theory C_Model_init imports Isabelle_Meta_Model.Printer_init - Citadelle.Old_Datatype + "HOL-Library.Old_Datatype" begin type_synonym int = integer