It’s nice that global theories don’t have to be qualified. But it’s a bit strange that it's forbidden to qualify them.
--lcp > On 2 Nov 2017, at 17:21, Makarius <makar...@sketis.net> wrote: > >> On 02/11/17 17:47, Lawrence Paulson wrote: >> >> And I have triple checked that Probability is spelt correctly. Any hints? > > Since Isabelle/f27488f47a47 you can use completion there (on the theory > base name). > > E.g. "ALi" completes "HOL-Library.AList". > > > Makarius _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
