Makarius wrote: > Its name indicates set operations, but it is now more general: > > listsp (inf (%x. x : ?A) (%x. x : ?B)) = > inf (%x. x : lists ?A) (%x. x : lists ?B) > > The recent change 1898e61e89c4 (berghofe) might be related. Stefan > should know what he had in mind.
If you look at the version of the tutorial available on the Isabelle web page (p. 141) http://isabelle.in.tum.de/dist/Isabelle2011-1/doc/tutorial.pdf you will see that it has already been broken for some time, the only difference being that set union is now printed as "inf", due to the recent re-introduction of the set type. When converting the rule listsp_inf_eq to set notation using inf_Int_eq, the resulting rule has the expected form: thm listsp_inf_eq [to_set inf_Int_eq] They were removed from the pred_set_conv database a while ago by Florian http://isabelle.in.tum.de/repos/isabelle/rev/7f9e05b3d0fb because they were considered "potentially dangerous", but now that sets and predicates can be distinguished again, this rule (and the dual rule sup_Un_eq) could be added again? Greetings, Stefan _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
