Quoting Makarius :
Does it mean you propose to discontinue "(in a)" at some point?
Exactly. Too early right now, but eventually this might make sense --
especially if the IDE provides suitable refactorings. Of course, this
wouldn't let us scrap a lot of code, but the Isar language could
On Sat, 27 Apr 2013, Florian Haftmann wrote:
fun gen_foo prep_1 … prep_n raw_x_1 … raw_x_n ctxt =
let
val x_1 = prep_1 ctxt raw_x_1;
…
val x_n = prep_n ctxt raw_x_n;
in
ctxt
|> …
end;
val foo = gen_foo cert_1 … cert_n;
val foo_cmd = gen_foo read_1 … read_n;
Here, raw
On Thu, 25 Apr 2013, Lars Noschinski wrote:
I just noticed (Isabelle rev. 30624dab6054) that "by" allows finishes a proof
(even if the proof is faulty), while ".." only finishes a proof if it can
actually prove the goal.
Is this intended behaviour or just an oversight?
It is a consequence o
On Tue, 21 May 2013, Lars Noschinski wrote:
On 21.05.2013 12:46, Makarius wrote:
An old idea on my list is to add some support to the Prover IDE to
rework theories with many consecutive "(in a)" to use just one "context
a begin ... end" around it -- this is also more efficient. Apart from
that
On 21.05.2013 12:46, Makarius wrote:
An old idea on my list is to add some support to the Prover IDE to
rework theories with many consecutive "(in a)" to use just one "context
a begin ... end" around it -- this is also more efficient. Apart from
that I have occasionally considered to provide expl
On Thu, 18 Apr 2013, Tobias Nipkow wrote:
I was under the impression that type synonyms are expanded in typ
antiquotations, but apparently not, at least not with 30624dab6054. If I write
@{typ vname} I get "vname", even if vname is a type synonym for string. Maybe it
has always been like this, b
Naturally this notation is less important than before, and never strictly
essential. But would we save much by eliminating it?
Larry
On 21 May 2013, at 11:46, Makarius wrote:
> Does it mean you propose to discontinue "(in a)" at some point?
>
> An old idea on my list is to add some support to
On Wed, 17 Apr 2013, Clemens Ballarin wrote:
Quoting Makarius :
That is just a matter of modularity of concepts: the older "(in a)"
notation was slightly generalized at some point to allow named contexts as
sketched above
In any case, I'm not sure how useful the old notation still is. Maybe
