Am 13.02.2014 12:48, schrieb Makarius:
Today isatest has reported a breakdown of HOL/Library/Code_Prolog.thy.
This was undetected in a more regular test due to this change that
removed it from the normal HOL-Library session:
changeset: 38504:76965c356d2a
user:haftmann
date:
Am 13.02.2014 um 13:19 schrieb Lawrence Paulson l...@cam.ac.uk:
I’m not sure what the question is any more. If it is about the choice of
names in Skolemization, that has been entirely redone in the past few years.
I imagine it is now something like this:
Subgoal.FOCUS (fn
I know it was a problem for machine learning that a free variable in a goal (x
say) might appear with multiple types in a problem set. This is connected with
the issue you’re describing now. I assume that that was solved somehow.
Larry
On 13 Feb 2014, at 12:31, Jasmin Blanchette
Hi Jasmin,
On 12/02/14 12:11, Jasmin Blanchette wrote:
Hi Andreas,
I saw that you used the discriminator =, but we already have functions
Option.is_none and List.null. So far, they have been mainly used for code generation, but
I have found them very convenient in in my codatatype usages
Hi Jasmin,
On 13/02/14 13:47, Jasmin Blanchette wrote:
Hi Andreas,
Am 13.02.2014 um 13:34 schrieb Andreas Lochbihler
andreas.lochbih...@inf.ethz.ch:
In summary, I do not want to replace _ = None and _ = [] with null and
is_none, I'd just like to make null and is_none somewhat official. I
Hi Andreas,
I read the comment to your changeset 3def821deb70, which says that Nat.pred
may show up in theorems generated by primcorec. This is fine, because the
destructor view for codatatypes goes well with discriminators and selectors
for datatypes. As I do not know where discriminators
On Thu, 13 Feb 2014, Dmitriy Traytel wrote:
So apart from some repairs of
src/HOL/Tools/Predicate_Compile/code_prolog.ML in a76c679c0218, the
changeset e42a3fc18458 makes more clear (in batch mode) that redefining
outer syntax commands is not supposed to happen. This provides a window
of
On Thu, 13 Feb 2014, Jasmin Blanchette wrote:
Am 13.02.2014 um 13:19 schrieb Lawrence Paulson l...@cam.ac.uk:
I’m not sure what the question is any more. If it is about the choice
of names in Skolemization, that has been entirely redone in the past
few years. I imagine it is now something
