# HG changeset patch # User wenzelm # Date 1525252310 -7200 # Wed May 02 11:11:50 2018 +0200 # Node ID d60436a866bb50ffbfc98598abd24160fdd37df6 # Parent d458a5cbda540b83c0d9920642c6e74bc8e5315d clarified imports for the sake of "hide_const (open) List.nth"; diff -r d458a5cbda54 -r d60436a866bb thys/HOLCF-Prelude/Definedness.thy --- a/thys/HOLCF-Prelude/Definedness.thy Wed May 02 10:49:26 2018 +0200 +++ b/thys/HOLCF-Prelude/Definedness.thy Wed May 02 11:11:50 2018 +0200 @@ -3,7 +3,6 @@ theory Definedness imports Data_List - "HOL-Library.Adhoc_Overloading" begin text \ diff -r d458a5cbda54 -r d60436a866bb thys/HOLCF-Prelude/HOLCF_Main.thy --- a/thys/HOLCF-Prelude/HOLCF_Main.thy Wed May 02 10:49:26 2018 +0200 +++ b/thys/HOLCF-Prelude/HOLCF_Main.thy Wed May 02 11:11:50 2018 +0200 @@ -4,6 +4,7 @@ imports HOLCF "HOLCF-Library.Int_Discrete" + "HOL-Library.Adhoc_Overloading" begin text \