Sorry was my mistake, should be fixed with d5a3dbc9da17 now. - Johannes
Am Sonntag, den 16.11.2014, 19:48 +0100 schrieb Florian Haftmann: > > isabelle: 059ba950a657 tip > > afp: 0fdf8f639bb4 tip > > Running JinjaThreads ... > > > > > > JinjaThreads FAILED > > (see also > > /mnt/home/haftmann/data/isabelle/master/heaps/polyml-5.5.2_x86-linux/log/JinjaThreads) > > > > *** At command "inductive" (line 413 of > > "/mnt/home/haftmann/data/afp/master/thys/JinjaThreads/Framework/FWLTS.thy") > > *** Type unification failed: No type arity prod :: floor_ceiling > > *** > > *** Type error in application: incompatible operand type > > *** > > *** Operator: floor :: ??'a => int > > *** Operand: (x, ln) :: ??'b * (real => real) > > *** > > *** Coercion Inference: > > *** > > *** Local coercion insertion on the operand failed: > > *** No type arity prod :: floor_ceiling > > *** > > *** Now trying to infer coercions globally. > > *** > > *** Coercion inference failed: > > *** weak unification of subtype constraints fails > > *** Clash of types "_ option" and "int" > > *** > > *** At command "inductive" (line 413 of > > "/mnt/home/haftmann/data/afp/master/thys/JinjaThreads/Framework/FWLTS.thy") > > Unfinished session(s): JinjaThreads > > 0:13:06 elapsed time, 1:00:51 cpu time, factor 4.64 > _______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
