Hi Andreas, > Let me ask something stupid: > why exactly do you guys axiomatize 'a set? > Sure it's admissable and all, but why not do this definitionally > via the obvious typedef?
the answer is rather technical: »typedef« in its current implementation
needs set syntax / set type as prerequisite. Of course you could change
»typedef« to be based on predicates, but there is some kind of unspoken
agreement not to set one's hand on that ancient and time-honoured Gordon
HOL primitive.
Rgds.,
Florian
--
Home:
http://www.in.tum.de/~haftmann
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
