Hi Lars, thanks for pointing this out, this was a serious slip in my work.
See now http://isabelle.in.tum.de/repos/isabelle/rev/f77b946d18aa Cheers, Florian Am 20.12.2016 um 17:50 schrieb Lars Hupel: > Dear Florian, > > you changed the representation of characters a while back, but it seems > like the Quickcheck setup is lacking a "full_exhaustive" instance. > > The stupidest possible workaround is > > quickcheck_generator char constructors: char_of_nat > > ... which I have just added locally to my theories. > > Maybe we should think about a proper implementation. > > Cheers > Lars > -- 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
