A further remark:
> 1.17 +definition ntrancl :: "('a * 'a => bool) => nat => ('a * 'a =>
> bool)"
> 1.18 +where
> 1.19 + [code del]: "ntrancl R n = (UN i : {i. 0 < i & i <= (Suc n)}. R ^^
> i)"
Canonically and keeping in mind the upcoming 'a set, this would be
definition ntrancl :: "nat => ('a * 'a) set => ('a * 'a) set"
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 [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
