I've just been trying to get the proofs working, not to simplify them or even
to understand them. Incidentally, let there be no illusions about people
accidentally stumbling into a mixture of sets and predicates. Some of these
theories were clearly designed from the ground upwards on the
Some notes concerning the following recent changes:
082edd97ffe1 huffman
comment out dead code to avoid compiler warnings
6f28f96a09bf huffman
avoid warnings
A priori, warnings are really just warnings, not errors.
When Poly/ML acquired this very useful warning for unused
maybe also declare them [no_atp], to avoid sledgehammer-generated proofs
that we know are going to break one release later...?
Maybe better now, as long as there are real sledgehammer-generated
proofs depending on it.
Florian
--
Home:
http://www.in.tum.de/~haftmann
PGP available:
Hi Larry,
And I'm finding it very difficult to work with two different versions of
Isabelle. I need to keep compiling one version or the other in order to
run tests. I know that we have ISABELLE_IDENTIFIER to eliminate that
problem, but it's empty in both versions.
I achieve this by having
I'm starting to have doubts about this entire procedure.
I thought the plan was to get these theories (particularly in the AFP) into a
state where they no longer dependent on confusing sets with predicates so
that they would work with either version of Isabelle. I'm not sure that's
A proof works only if I insert before it the following:
instance set :: (type) complete_boolean_algebra
proof
qed (auto simp add: INF_def SUP_def Inf_set_def Sup_set_def Inf_bool_def
Sup_bool_def)
this is strange because this exact text already appears in the file
Complete_Lattice.thy
This suggestion looks promising. However, my impression is that
ISABELLE_OUTPUT specifies where images will be written to. Does it also
specify where images (unless a full path is specified) are read from? I often
seem to get the wrong image unless I rename them manually, which is obviously
Hi all,
Shouldn't one remove quite a bit of duplication first? The classes
distributive_complete_lattice and complete_boolean_algebra are now part
of HOL (the former as complete_distrib_lattice) (see the FIXME). The set
instances for those should be in/go into Florian's HOL repository as
