[isabelle-dev] Update of Haskell Stack

2018-12-28 Thread Makarius
Here are some notable changes concerning the Haskell Stack, which is a build tool with a package repository behind it: changeset: 69526:5574d504cf36 tag: tip user:wenzelm date:Fri Dec 28 19:01:35 2018 +0100 files: etc/settings description: more conservative update

Re: [isabelle-dev] cardinality primitives in Isabelle/HOL?

2018-12-28 Thread Lawrence Paulson
Tons of useful stuff here. Some syntactic ambiguities, particularly around the =o relation, which is also defined as Set_Algebras.elt_set_eq. I don’t suppose there’s any chance of using quotients to define actual cardinals and use ordinary equality? And it still makes sense to introduce the