I am under the impression that the AFP is currently lagging behind, e.g. isabelle: 5bee93b2020d tip afp: c677a10107a6 tip
Any changesets awaiting a push somewhere?
Florian
> Tycon FAILED
> (see also
> /mnt/home/haftmann/data/isabelle/devel/heaps/polyml-5.5.2_x86-linux/log/Tycon)
>
> *** Failed to load theory "Binary_Tree_Monad" (unresolved "Monad")
> *** Failed to load theory "Lift_Monad" (unresolved "Monad")
> *** Failed to load theory "Monad_Plus" (unresolved "Monad")
> *** Failed to load theory "Monad_Zero" (unresolved "Monad")
> *** Failed to load theory "Writer_Monad" (unresolved "Monad")
> *** Failed to load theory "Error_Monad" (unresolved "Monad_Plus")
> *** Failed to load theory "Monad_Zero_Plus" (unresolved "Monad_Plus",
> "Monad_Zero")
> *** Failed to load theory "Lazy_List_Monad" (unresolved "Monad_Zero_Plus")
> *** Failed to load theory "Maybe_Monad" (unresolved "Monad_Zero_Plus")
> *** Failed to load theory "State_Transformer" (unresolved "Monad_Zero_Plus")
> *** Failed to load theory "Error_Transformer" (unresolved "Error_Monad")
> *** Failed to load theory "Writer_Transformer" (unresolved "Writer_Monad")
> *** Failed to load theory "Resumption_Transformer" (unresolved "Monad_Plus")
> *** Missing outer syntax command(s) "tycondef"
> *** ML error (line 397 of
> "/mnt/home/haftmann/data/afp/devel/thys/Tycon/tycondef.ML"):
> *** Value or constructor (axiomatize_arity) has not been declared in
> structure Axclass
> *** ML error (line 803 of
> "/mnt/home/haftmann/data/afp/devel/thys/Tycon/tycondef.ML"):
> *** Value or constructor (axiomatize_arity) has not been declared in
> structure Axclass
> ***
> *** At command "ML_file" (line 223 of
> "/mnt/home/haftmann/data/afp/devel/thys/Tycon/Functor.thy")
--
PGP available:
http://home.informatik.tu-muenchen.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
