I am currently working on AFP/Coinductive, which is full of the sort of thing. Larry
On 19 Aug 2011, at 00:31, Gerwin Klein wrote: > Can't really quantify it, but I'm seeing this all the time from not-so-novice > users over here. Mixing sets and predicates (e.g. using intersection on > predicates) works often enough that people like it and overuse it. Sooner or > later you will see unfolding of mem_def. As opposed to unfolding conjunction, > unfolding mem_def proves things that otherwise simp/auto/etc fail on. _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
