[isabelle-dev] NEWS: HOL/Library/Omega_Words_Fun

2015-09-15 Thread Peter Lammich
* 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

Re: [isabelle-dev] JinjaThreads

2015-09-15 Thread Andreas Lochbihler
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

Re: [isabelle-dev] NEWS: HOL/Library/Omega_Words_Fun

2015-09-15 Thread Makarius
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

Re: [isabelle-dev] JinjaThreads

2015-09-15 Thread Andreas Lochbihler
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

[isabelle-dev] JinjaThreads

2015-09-15 Thread Makarius
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