Am 25/11/2011 16:56, schrieb Makarius:
Broken proof methods
sos_cert
some uses in Library/Sum_of_Squares.thy
BTW the regular sos method with the server communication is broken for
some months already. It would be nice if someone could volunteer to
recover this nice student project
On Thu, 24 Nov 2011, Brian Huffman wrote:
I have been working on a new numeral representation for Isabelle
recently, and I would like to share it with everyone. An overview of the
design is now available on the Isanotes wiki [1]; a patched version of
the Isabelle hg repo is also available
Hi Brian,
I have been working on a new numeral representation for Isabelle
recently, and I would like to share it with everyone. An overview of
the design is now available on the Isanotes wiki [1]; a patched
version of the Isabelle hg repo is also available [2].
I would welcome any
class neg_numeral = group_add + one
definition (in neg_numeral) neg_numeral :: bin = 'a where
neg_numeral k = - numeral k
Is there a conceptual point for neg_numeral, beyond concrete syntax issues?
One could just use regular uminus, but then there will be an accidental
change in
Hi all,
I have been working on a new numeral representation for Isabelle
recently, and I would like to share it with everyone. An overview of
the design is now available on the Isanotes wiki [1]; a patched
version of the Isabelle hg repo is also available [2].
[1]
