*** Isar ***
* Toplevel theorem statements support eigen-context notation with 'if' /
'for' (in postix), which corresponds to 'assumes' / 'fixes' in the
traditional long statement form (in prefix). Local premises are called
"that" or "assms", respectively. Empty premises are *not* bound in the
con
*** General ***
* Embedded content (e.g. the inner syntax of types, terms, props) may be
delimited uniformly via cartouches. This works better than old-fashioned
quotes when sub-languages are nested.
*** Prover IDE -- Isabelle/Scala/jEdit ***
* Cartouche abbreviations work both for " and ` to a
On 03/04/16 14:50, Lawrence Paulson wrote:
> The DIM('a) notation is introduced in Multivariate_Analysis/Euclidean_Space,
> for referring to the dimension of the Euclidean space designated by type ‘a.
> (See code snippet below.) Unfortunately, DIM(‘a) pretty-prints as card Basis,
> and the type
On 20/03/16 06:41, Lars Noschinski wrote:
> On 11.03.2016 18:37, Makarius wrote:
>> * The executable "isabelle_process" has been discontinued. Tools and
>> prover front-ends should use ML_Process or Isabelle_Process in
>> Isabelle/Scala. INCOMPATIBILITY.
>>
>> * New command-line tool "isabelle proc
Argh! You are correct. Today is /not/ my day. I'm on it.
On 24/05/16 18:42, Makarius wrote:
On 24/05/16 18:34, Manuel Eberl wrote:
I'm confident that I'll have everyting up and running again soon.
BTW, current Isabelle/8230358fab88 now looks like too much has been
committed.
Makariu
On 24/05/16 18:34, Manuel Eberl wrote:
> I'm confident that I'll have everyting up and running again soon.
BTW, current Isabelle/8230358fab88 now looks like too much has been
committed.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tu
Yes, this was my fault. The problem was that I stupidly forgot to commit
my changes before I pushed to the testboard and thus did not see the
problems caused by my changes.
I'm confident that I'll have everyting up and running again soon.
Manuel
On 24/05/16 17:22, Jasmin Blanchette wrote:
O
On 24.05.2016, at 17:12, Makarius wrote:
>
> The Isabelle repository is broken at 76cb6c6bd7b8 (paulson) or
> 6a17bcddd6c2 (eberlm).
>
> The failure is as follows:
> ### theory "Generate_Binary_Nat"
> ### 197.201s elapsed time, 259.420s cpu time, 8.924s GC time
> *** "List.coset" is not a constr
> https://ci.isabelle.systems/jenkins shows many dark clouds and
> thunderbolts, but I have no clue where to look precisely.
Jenkins is a complex piece of software (much more complex than
Isabelle), so it is indeed hard to figure out where to click.
The best way to stay on top of the current stat
I did run a full test of my changes, which in any event don’t look connected
with the error message you report.
Larry
> On 24 May 2016, at 16:12, Makarius wrote:
>
> The Isabelle repository is broken at 76cb6c6bd7b8 (paulson) or
> 6a17bcddd6c2 (eberlm).
>
> The failure is as follows:
> ### the
The Isabelle repository is broken at 76cb6c6bd7b8 (paulson) or
6a17bcddd6c2 (eberlm).
The failure is as follows:
### theory "Generate_Binary_Nat"
### 197.201s elapsed time, 259.420s cpu time, 8.924s GC time
*** "List.coset" is not a constructor, on left hand side of equation, in
theorem:
*** permu
11 matches
Mail list logo
