On 08/24/2011 03:36 PM, Lawrence Paulson wrote:
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
On Wed, 24 Aug 2011, Florian Haftmann wrote:
I was driven crazy some months ago when I attempted in vain to enable
push access. I don't even know what the problem was (authentication,
web server configuration, encrpytion) – maybe I wasn't even able to
figure out. If someone of the TUM guys
Since August is the canonical time for vacation for many people it is
probably better to get into more concrete discussions in 3-4 weeks from
now, but people can already start thinking about their own areas of
responsibility concerning consolidation for the release.
I have two topics on the
When I've seen the complete_boolean_algebra incident on the other
thread my first impulse was to check how far the wiring of the class
package wrt. the Isabelle document markup was. In principle the prover
can provide useful clues in non-intrusive ways here, if done right.
E.g. in
(BTW, in
Scala ambiguity after additional imports is treated as an error, and
causes the conflicting name entries to be canceled out.)
I definitely like this!
Florian
--
Home:
http://www.in.tum.de/~haftmann
PGP available:
Should we ask a wider audience (isabelle-users) if anybody else has good
reasons against/for a change?
The thought deserves attention, but I think the discussion is too early
for that.
Indeed, this is where, as I deem, we current are:
* Some agreement that mixing sets and predicate syntax in
Hi all,
thanks to many efforts (thanks particularly to Alex, Brian, Cezary,
Larry) we already have gained some insights whether and how it would be
technically possible to introduce a set type constructor.
As I see the whole story, we have to think carefully how we would
proceed in order to
Hi Jasmin,
HOL-Metis_Examples FAILED
HOL-Nitpick_Examples FAILED
I can look into those things if and when it is decided to move to sets.
in case, thanks for the offer. Please ignore any further announcements
of these sessions in intermediate reports ;-).
Florian
--
Home:
On 08/25/2011 10:45 PM, Florian Haftmann wrote:
Hi all,
thanks to many efforts (thanks particularly to Alex, Brian, Cezary,
Larry) we already have gained some insights whether and how it would be
technically possible to introduce a set type constructor.
Let me ask something stupid:
why
Hi all,
I remember that once there was a discussion how AFP theories could be
referenced in theory headers using an environment variable AFP_THEORIES
or something similar.
Maybe the afp could be turned into an optional Isabelle component, e.g.
at ~~/contrib/afp. This would be have a couple of
On 08/25/2011 11:26 PM, Florian Haftmann wrote:
Hi Andreas,
Let me ask something stupid:
why exactly do you guys axiomatize 'a set?
Sure it's admissable and all, but why not do this definitionally
via the obvious typedef?
the answer is rather technical: »typedef« in its current
On 26/08/11 7:26 AM, Florian Haftmann wrote:
Hi Andreas,
Let me ask something stupid:
why exactly do you guys axiomatize 'a set?
Sure it's admissable and all, but why not do this definitionally
via the obvious typedef?
the answer is rather technical: »typedef« in its current
-BEGIN PGP SIGNED MESSAGE-
Hash: SHA1
On 26/08/2011, at 7:23 AM, Florian Haftmann wrote:
I remember that once there was a discussion how AFP theories could be
referenced in theory headers using an environment variable AFP_THEORIES
or something similar.
Maybe the afp could be turned
Hi,
I'm trying to generate a proof goal from string using the following:
fun generate x lthy =
let
val thy = Local_Theory.exit_global lthy
val ctxt = ProofContext.init_global thy
in
(Specification.theorem_cmd
Thm.lemmaK NONE (K I)
14 matches
Mail list logo
