There is another drop-out concerning 'a set (in Isabelle/05a82dd869ed):
inductive_set
well_formed_gterm' :: "('f \<Rightarrow> nat) \<Rightarrow> 'f gterm set"
for arity :: "'f \<Rightarrow> nat"
where
step[intro!]: "\<lbrakk>args \<in> lists (well_formed_gterm' arity);
length args = arity f\<rbrakk>
\<Longrightarrow> (Apply f args) \<in> well_formed_gterm' arity"
monos lists_mono
*** Bad monotonicity theorem:
*** {x. ?A x} <= {x. ?B x} ==> {x. listsp ?A x} <= {x. listsp ?B x}
*** At command "inductive_set" (line 153 of
"~~/doc-src/TutorialI/Inductive/Advanced.thy")
That is probably a bit too exotic to expect NEWS to say what needs to be
done. Nonetheless I am curious about the reason of this failure.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
