* Command 'subgoal' allows to impose some structure on backward
refinements, to avoid proof scripts degenerating into long of 'apply'
sequences. Further explanations and examples are given in the isar-ref
manual.
This refers to Isabelle/441fdbfbb2d3, which also contains the
documentation and
On Tue, 30 Jun 2015, Lars Noschinski wrote:
Moreover note, that the above example provides a solution to the
occasional problem of ?thesis1, ?thesis2, etc. -- which are not
provided by the system. It just becomes ?case in each case.
I'd say this is a partial solution: When I have a situation
I like the dots notation, it resolves the issue of having to always think about
the parameters in reverse order.
I've found a few small issues related to clashing/fresh names.
First, It looks like the suffix naming doesn't quite work if there are clashing
existing goal params.
e.g.
lemma ⋀x
On 03.07.2015 04:02, Daniel Matichuk wrote:
Additionally, fresh names are chosen for any free variables that appear in
the subgoal
e.g.
lemma ⋀x y. A x y
subgoal for A
Results in x being named Aa. In this case I would expect either an error
(Free name clash) or for the new fixed
On Thu, 2 Jul 2015, Joachim Breitner wrote:
I was curious about the new subgoal command, so I wonder: Is the built
documentation of the current development snapshot readily available
online somewhere? I was looking at http://isabelle.in.tum.de/devel/ and
would not find it there.
For
On Fri, 26 Jun 2015, Makarius wrote:
On Fri, 26 Jun 2015, Larry Paulson wrote:
HOL-Proofs, etc., have been failing for several days now. Last time I
checked, it was simply a timeout. Presumably some change to rewriting is
to blame. It may be similar to the AFP failure that I fixed
