Tobias
On 18/06/2017 20:38, Florian Haftmann wrote:
isabelle: 20304512a33b tip afp: 644957b424ee tip JinjaThreads FAILED (see also /srv/data/tum/isabelle/master/heaps/polyml-5.6_x86-linux/log/JinjaThreads) *** (\<forall>T. *** typeof\<^bsub>h\<^esub> v = *** \<lfloor>T\<rfloor> \<longrightarrow> *** (\<forall>C. *** class_type_of' T = *** \<lfloor>C\<rfloor> \<longrightarrow> *** (\<forall>Ts Tr D. *** P \<turnstile> C sees M: Ts\<rightarrow>Tr = Native in D \<longrightarrow> *** \<tau>external_defs D M)))) *** then (\<tau>red0t (extTA2J0 P) P t h *** (Val v\<bullet>M(es), xs) *** (Val v\<bullet>M(es'), xs') \<or> *** countInitBlock (Val v\<bullet>M(es1')) *** < countInitBlock (Val v\<bullet>M(es1)) \<and> *** Val v\<bullet>M(es') = *** Val v\<bullet>M(es) \<and> *** xs' = xs) \<and> *** h' = h \<and> *** ta1 = \<lbrace>\<rbrace> \<and> *** ta = \<lbrace>\<rbrace> *** else ta_bisim01 ta (extTA2J1 (compP1 P) ta1) \<and> *** (if call (Val v\<bullet>M(es)) = None \<or> *** call1 (Val v\<bullet>M(es1)) = None *** then \<exists>e'' xs''. *** \<tau>red0r (extTA2J0 P) P t h *** (Val v\<bullet>M(es), xs) (e'', xs'') \<and> *** extTA2J0 *** P,P,t \<turnstile> \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> *** \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> *** no_call P h e'' \<and> *** \<not> \<tau>move0 P h e'' *** else extTA2J0 *** P,P,t \<turnstile> \<langle>Val *** v\<bullet>M(es), *** (h, xs)\<rangle> -ta\<rightarrow> *** \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> *** no_call P h (Val v\<bullet>M(es)) \<and> *** \<not> \<tau>move0 P h *** (Val v\<bullet>M(es)))) *** At command "apply" (line 911 of "/srv/data/tum/afp/master/thys/JinjaThreads/Compiler/Correctness1.thy")Any hint what is going on? Cheers, Florian _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
