Re: [isabelle-dev] [isabelle] Code setup for Fraction_Field

Hi Florian, I am continuing this thread on isabelle-dev as you have suggested. 3. For fraction fields over polynomials over rings (rather than fields), one can use subresultants, but I have not been able to find them formalised in Isabelle. Are they hidden somewhere? If not, are there any

[isabelle-dev] ML equality types

In src/Pure/library.ML, the signature still contains the discouraged and nowadays rarely used entries val equal: ''a -> ''a -> bool val not_equal: ''a -> ''a -> bool Shall we attempt to get rid of them finally? Florian -- PGP available:

Re: [isabelle-dev] Code generation to OCaml and Scala

Hi Fréderic, see now http://isabelle.in.tum.de/repos/isabelle/rev/774752af4a1f http://isabelle.in.tum.de/repos/isabelle/rev/8e736ce4c6f4 >> By comparing the generating code for SML and OCaml in >> src/Tools/Code/code_ml.ML, I would be tempted to replace >> "brackify_block" by "brackets"

Re: [isabelle-dev] NEWS

Hi Dmitriy, > while I very much welcome the simplified printing rules and your effort > of unifying case_prod/split, I am not sure if adding a third alternative > name is the way to go. The situation reminds me of the one depicted in [1]. the other two are mere input abbreviations, which could

[isabelle-dev] NEWS

* Combinator to represent case distinction on products is named "uncurry", with "split" and "prod_case" retained as input abbreviations. Partially applied occurences of "uncurry" with eta-contracted body terms are not printed with special syntax, to provide a compact notation and getting rid of a

Re: [isabelle-dev] NEWS

Hi Florian, while I very much welcome the simplified printing rules and your effort of unifying case_prod/split, I am not sure if adding a third alternative name is the way to go. The situation reminds me of the one depicted in [1]. Clearly, case_prod is the "right" name from the perspective

Re: [isabelle-dev] NEWS

I hope you will also restore the printing of "λ(x,y). x+y" as "λ(x,y). x+y" rather than "uncurry op +". Tobias On 10/09/2015 12:48, Florian Haftmann wrote: Hi Andreas, I noticed that the new printing interacts strangely with set comprehensions. In Isabelle/92858a52e45b, "{(x, y). P x y}"

Re: [isabelle-dev] NEWS

Hi Andreas, > I noticed that the new printing interacts strangely with set > comprehensions. In Isabelle/92858a52e45b, "{(x, y). P x y}" prints as > "Collect (uncurry P)" which I find rather hard to read. Are you aware of > this effect and could you please restore the former situation? this is

Re: [isabelle-dev] ML equality types

I can't see any specific benefit of doing this. I still think that the next big project of this kind should be to sort out the real/of_nat mess. I’ve proposed an approach to doing it, but haven’t yet found a sufficient block of time in which executed. Larry > On 10 Sep 2015, at 11:31, Florian

Re: [isabelle-dev] NEWS

Purely FYI: the names of all of these constants were originally based on the corresponding names in Martin-Löf type theory. Larry > On 10 Sep 2015, at 12:34, Tobias Nipkow wrote: > > > On 10/09/2015 12:19, Dmitriy Traytel wrote: >> Hi Florian, >> >> while I very much

Re: [isabelle-dev] NEWS

> I hope you will also restore the printing of "λ(x,y). x+y" as "λ(x,y). > x+y" rather than "uncurry op +". Okay, this is really unpleasant. Thanks for reporting this. Florian > > Tobias > > On 10/09/2015 12:48, Florian Haftmann wrote: >> Hi Andreas, >> >>> I noticed that the new

Re: [isabelle-dev] NEWS

Hi Florian, I noticed that the new printing interacts strangely with set comprehensions. In Isabelle/92858a52e45b, "{(x, y). P x y}" prints as "Collect (uncurry P)" which I find rather hard to read. Are you aware of this effect and could you please restore the former situation? Best,

Re: [isabelle-dev] NEWS

On 10/09/2015 12:19, Dmitriy Traytel wrote: Hi Florian, while I very much welcome the simplified printing rules and your effort of unifying case_prod/split, I am not sure if adding a third alternative name is the way to go. The situation reminds me of the one depicted in [1]. Clearly,

Re: [isabelle-dev] NEWS

On 10.09.2015 12:19, Dmitriy Traytel wrote: > Hi Florian, > > while I very much welcome the simplified printing rules and your effort > of unifying case_prod/split, I am not sure if adding a third alternative > name is the way to go. The situation reminds me of the one depicted in [1]. > >

Re: [isabelle-dev] NEWS

On Thu, 10 Sep 2015, Larry Paulson wrote: Purely FYI: the names of all of these constants were originally based on the corresponding names in Martin-Löf type theory. I do remember the good old times of MLTT, where it was clear what the basic combinators are. Interestingly, MLTT is

Re: [isabelle-dev] ML equality types

On Thu, 10 Sep 2015, Florian Haftmann wrote: In src/Pure/library.ML, the signature still contains the discouraged and nowadays rarely used entries val equal: ''a -> ''a -> bool val not_equal: ''a -> ''a -> bool These operations are a bit old-fashioned, but why are they