See now finally http://isabelle.in.tum.de/repos/isabelle/rev/a41435469559
Florian
Am 23.06.2017 um 08:43 schrieb Lars Hupel:
>> The patch is now running on testboard:
>> <https://ci.isabelle.systems/jenkins/job/testboard/385/>.
>
> Unfortunately, this patch did not work out.
>
> 22:13:39 *** Failed to finish proof (line 62 of
> "~~/src/HOL/Library/Code_Target_Nat.thy"):
> 22:13:39 *** goal (1 subgoal):
> 22:13:39 *** 1. Transfer.Rel (rel_fun pcr_integer (rel_fun op = op =))
> 22:13:39 *** (\<lambda>a b. True) op =
> 22:13:39 *** At command "by" (line 62 of
> "~~/src/HOL/Library/Code_Target_Nat.thy")
>
--
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
