haftmann [Wed, 04 Mar 2009 13:41:59 +0100] rev 30248
datatype antiquotation does not assume LaTeX as output any longer
nipkow [Wed, 04 Mar 2009 11:49:12 +0100] rev 30247
merged
nipkow [Wed, 04 Mar 2009 11:48:52 +0100] rev 30246
Option.thy
haftmann [Wed, 04 Mar 2009 11:44:05 +0100] rev 30245
consequent rewrite of index_size, size [index] to nat_of; support pseudo-primrec sepcifications with fun
haftmann [Wed, 04 Mar 2009 11:37:50 +0100] rev 30244
merged
haftmann [Wed, 04 Mar 2009 10:52:47 +0100] rev 30243
explicit error message for `improper` instances lacking explicit instance parameter constants
blanchet [Wed, 04 Mar 2009 11:05:29 +0100] rev 30242
Merge.
blanchet [Wed, 04 Mar 2009 11:05:02 +0100] rev 30241
Merge.
blanchet [Wed, 04 Mar 2009 10:45:52 +0100] rev 30240
Merge.
blanchet [Wed, 04 Mar 2009 10:43:39 +0100] rev 30239
Made Refute.norm_rhs public, so I can use it in Nitpick.
blanchet [Sun, 01 Mar 2009 18:40:16 +0100] rev 30238
Added "nitpick_const_def" attribute, for overriding the definition axiom of a constant.
blanchet [Tue, 24 Feb 2009 16:12:27 +0100] rev 30237
Eliminated ZCHAFF_VERSION configuration variable, since zChaff's output format is identical in all versions since March 2003 (at least), and also because it forces users who want to use the latest versions to lie about the version number.
I also made the BERKMIN_EXE variable optional, defaulting to BerkMin561 (a reasonable name with no platform encoded in it).
These changes have no inpacts on already working Isabelle installations.
nipkow [Wed, 04 Mar 2009 10:47:35 +0100] rev 30236
merged
nipkow [Wed, 04 Mar 2009 10:47:20 +0100] rev 30235
Made Option a separate theory and renamed option_map to Option.map