* HOL/Library/Omega_Words_Fun: Infinite words modeled as
functions nat => 'a.
This lived hidden in $AFP/Automatic_Refinement before, but other entries
started to use it. So I moved it to HOL/Library.
(Expecting $AFP/LTL_to_DRA to break until Salomon, who wants to adapt it
himself, has fixed
Hi Makarius,
This might be due to my attempt to repair Predicate_Compile_Examples in 78ece168f5b5. I'll
see what I can do.
Andreas
On 15/09/15 16:41, Makarius wrote:
This is the situation in Isabelle/0b071f72f330 and AFP/3085eb9e2bb9:
*** Failed to load theory "Execute_Main" (unresolved
On Tue, 15 Sep 2015, Peter Lammich wrote:
* HOL/Library/Omega_Words_Fun: Infinite words modeled as
functions nat => 'a.
This lived hidden in $AFP/Automatic_Refinement before, but other entries
started to use it. So I moved it to HOL/Library.
This refers to Isabelle/0b071f72f330. On
It should work now again (Isabelle/e4716b792713 and AFP/ec3887abf158).
Sorry for the trouble,
Andreas
On 15/09/15 16:41, Makarius wrote:
This is the situation in Isabelle/0b071f72f330 and AFP/3085eb9e2bb9:
*** Failed to load theory "Execute_Main" (unresolved "Java2Jinja")
*** Failed to load
This is the situation in Isabelle/0b071f72f330 and AFP/3085eb9e2bb9:
*** Failed to load theory "Execute_Main" (unresolved "Java2Jinja")
*** Failed to load theory "JinjaThreads" (unresolved "Execute_Main")
*** Dependency "member_i_i" -> "case_list" would result in module dependency
cycle
*** At