[isabelle-dev] Relations vs. Predicates
Hi all,
currently there are two constants
op ^ :: 'b = nat = 'b
op ^^ :: 'b = nat = 'b
making it a bit difficult for the user to choose the correct one in all
situations. As far as I see op ^^ is just syntax for the overloaded
compow. Shouldn't it be possible to unify this (and also relpow) by
using adhoc overloading, so that only one operator, e.g., op ^ remains?
To come back to the subject, I'm missing iteration of predicates,
i.e., what _^^n is on relations but for predicates ('a = 'a =
bool). (Why are predicates less developed than relations anyway?)
cheers
chris
PS: I suggest to rename rel_comp into relcomp (to be consistent with
relpow). In @{theory Relation} there is a typo in the lemma name
prod_comp_bot1.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Towards the next release
On Fri, 16 Mar 2012, Florian Haftmann wrote: * The set story: https://isabelle.in.tum.de/community/Having_%27a_set_back Not everything mentioned there is an ultimate need, but we should strive to pick as many fruits as we can from the set type constructor – the more likely this will compensate users if they have to adjust their theories * The numeral story: https://isabelle.in.tum.de/community/Numerals It looks quite good (preliminary tests of the AFP did not reveal much problems). The fork should be done by the end of April. The further perspectives listed there are no need-to-haves for the next release. Does it mean both will reforms will be finished for the coming release? Makarius___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] jar: command not found
Hi, When the JDK is not given in the PATH variable, the command isabelle jedit may fail with ./build-jars: line 189: jar: command not found This is at least the case for hg id 08c22e8ffe70. The problem occurs with Cygwin where the JDK is provided as a component in the Isabelle bundle and is hence typically not mentioned in the PATH. Proper prefixing of invocations of jar with the JDK's path might solve this issue. Cheers, Sascha ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
