> 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
--
PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
