On Wed, 24 Jun 2015, Makarius wrote:
After seeing too many "case 1", "case 2", "case 3" and corresponding
facts "1", "2", "3" I've now pushed this trivial change through, really
with rare incompatibilities.
Here is an example changeset that illustrates the reduction of odd digits
and redunda
* Command 'case' allows fact name and attribute specification like this:
case a: (c xs)
case a [attributes]: (c xs)
Facts that are introduced by invoking the case context are uniformly
qualified by "a"; the same name is used for the cumulative fact. The old
form "case (c xs) [attributes]" is
* Local goals ('have', 'show', 'hence', 'thus') allow structured
statements like fixes/assumes/shows in theorem specifications, but the
notation is postfix with keywords 'if' (or 'when') and 'for'. For
example:
have result: "C x y"
if "A x" and "B y"
for x :: 'a and y :: 'a
The lo
* Method "sleep" succeeds after a real-time delay (in seconds). This is
occasionally useful for demonstration and testing purposes.
This refers to Isabelle/c0e1c121c7c0.
Maybe a bit silly, but in experimentation with Eisbach and parallel
evaluation, it turned out surprisingly difficult to get
* Nesting of Isar goal structure has been clarified: the context after
the initial backwards refinement is retained for the whole proof, within
all its context sections (as indicated via 'next'). This is e.g.
relevant for 'using', 'including', 'supply':
have "A ∧ A" if a: A for A
supply [si
On Wed, 24 Jun 2015, Larry Paulson wrote:
This may be the problem. I don’t remember exactly what I was trying to
do, only that it was very difficult. Of course nobody uses show_types
any more. Larry
On 24 Jun 2015, at 15:13, Dmitriy Traytel wrote:
You can hover in the output panel, but you
This may be the problem. I don’t remember exactly what I was trying to do, only
that it was very difficult. Of course nobody uses show_types any more.
Larry
> On 24 Jun 2015, at 15:13, Dmitriy Traytel wrote:
>
> You can hover in the output panel, but you won't see types of constants there.
___
On 24.06.2015 16:29, Larry Paulson wrote:
> This may be the problem. I don’t remember exactly what I was trying to do,
> only that it was very difficult. Of course nobody uses show_types any more.
At least this was the problem for me. A notorious instance of the same
problem are the functions in H
Ah, I see the problem. In that case, one could still hover over the
"of_nat" in the output window, but it is perhaps not ideal.
On 24/06/15 16:08, Dmitriy Traytel wrote:
I guess what Larry means is there is no way to see a type of a
constant that is not there in the source.
Consider e.g.
de
You can hover in the output panel, but you won't see types of constants
there.
Dmitriy
On 24.06.2015 16:09, Manuel Eberl wrote:
Ah, I see the problem. In that case, one could still hover over the
"of_nat" in the output window, but it is perhaps not ideal.
On 24/06/15 16:08, Dmitriy Traytel
I guess what Larry means is there is no way to see a type of a constant
that is not there in the source.
Consider e.g.
declare [[coercion "of_nat :: nat ⇒ real"]]
term "sqrt (2 :: nat)"
Today the output says "sqrt (real_of_nat 2)". But if there would be no
abbreviation for "of_nat :: nat ⇒ re
On 24/06/15 15:55, Larry Paulson wrote:
A more appropriate point is that it can be tricky in Isabelle/jEdit to
determine the type of an expression such as “of_nat k”, as there is nothing to
click on.
When I type ‘term "sqrt (of_nat 2)"’ and hover over the ‘of_nat’, it
says ‘constant "Nat.semir
The first question is, do we need a prefix syntax for type constraints? My
point was that the ability to write
[:real:]of_nat k
might be better than having to introduce and abbreviations such as real_of_nat,
but this is not clear. The latter has the advantage that it is automatically
i
13 matches
Mail list logo
