In Isabelle2016-RC4 I’ve noticed that there is a small but significant issue with how the “subgoal” command handles meta-conjuncts.
I have a method which folds subgoals into meta conjunctions, which is effectively the reverse of Goal.conjunction_tac. The intention is that you can collapse several subgoals into one for the purposes of discharging them with “subgoal”. Example: lemma assumes A: A and B: B and C: C shows "A ∧ B ∧ C" apply (intro conjI) apply fold_subgoals[2] subgoal by (auto intro: A B) apply (rule C) done This worked in my old implementation of subgoal, but I have recently discovered that “subgoal” (Isabelle2016) is introducing the conjunction before focusing. This results in only focusing on the first conjunct, instead of the entire meta-conjunct. The obvious solution from my end is to have “fold_subgoals” use a custom meta-connective that needs to be explicitly introduced after the “subgoal”, but I was wondering if it would be possible to postpone the meta-conjuction introduction until after the subgoal focus. -Dan ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
