Sun, 01 Mar 2009 18:40:16 +0100Added "nitpick_const_def" attribute, for overriding the definition axiom of a constant.
blanchet [Sun, 01 Mar 2009 18:40:16 +0100] rev 30238
Added "nitpick_const_def" attribute, for overriding the definition axiom of a constant.

Tue, 24 Feb 2009 16:12:27 +0100Eliminated 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.
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.

Wed, 04 Mar 2009 10:47:35 +0100merged
nipkow [Wed, 04 Mar 2009 10:47:35 +0100] rev 30236
merged

Wed, 04 Mar 2009 10:47:20 +0100Made Option a separate theory and renamed option_map to Option.map
nipkow [Wed, 04 Mar 2009 10:47:20 +0100] rev 30235
Made Option a separate theory and renamed option_map to Option.map

Wed, 04 Mar 2009 00:05:20 +0100renamed Method.assumption_tac back to Method.assm_tac -- as assumption_tac it would have to be exactly the tactic behind the assumption method (with facts);
wenzelm [Wed, 04 Mar 2009 00:05:20 +0100] rev 30234
renamed Method.assumption_tac back to Method.assm_tac -- as assumption_tac it would have to be exactly the tactic behind the assumption method (with facts);

Tue, 03 Mar 2009 21:53:52 +0100eliminated internal stamp equality, replaced by bare-metal pointer_eq;
wenzelm [Tue, 03 Mar 2009 21:53:52 +0100] rev 30233
eliminated internal stamp equality, replaced by bare-metal pointer_eq;
misc tuning and polishing;

Tue, 03 Mar 2009 21:49:34 +0100tuned str_of, now subject to verbose flag;
wenzelm [Tue, 03 Mar 2009 21:49:34 +0100] rev 30232
tuned str_of, now subject to verbose flag;

Tue, 03 Mar 2009 21:49:05 +0100added @{binding} ML antiquotations;
wenzelm [Tue, 03 Mar 2009 21:49:05 +0100] rev 30231
added @{binding} ML antiquotations;

Tue, 03 Mar 2009 21:48:40 +0100added print_properties, print_position (again);
wenzelm [Tue, 03 Mar 2009 21:48:40 +0100] rev 30230
added print_properties, print_position (again);

Tue, 03 Mar 2009 19:30:43 +0100merged
wenzelm [Tue, 03 Mar 2009 19:30:43 +0100] rev 30229
merged