Is the following behaviour really a good idea and useful? inductive P :: "nat => bool" where "P(suc n)"
is accepted but defines P :: "'a itself => nat => bool" It does kind of warn me by saying ### Additional type variable(s) in specification of P: 'a but if you miss that warning, you will be very surprised about the kind of errors you get later on when using P. If I give a constant an explicit type, I would prefer Isabelle to respect that. Tobias _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
