wenzelm [Thu, 05 Mar 2009 02:27:54 +0100] rev 30272
regenerated document;
wenzelm [Thu, 05 Mar 2009 02:24:36 +0100] rev 30271
merge with dummy changeset, to recover files in doc-src/IsarImplementation/ which got lost in aea5d7fa7ef5 (potentially due to insensitive file system on Mac OS);
wenzelm [Thu, 05 Mar 2009 02:20:06 +0100] rev 30270
dummy changes to produce a new changeset of these files;
wenzelm [Thu, 05 Mar 2009 01:55:38 +0100] rev 30269
updated generated file -- changed since @{ML} now ignores source flag;
wenzelm [Thu, 05 Mar 2009 00:16:28 +0100] rev 30268
fixed document;
wenzelm [Wed, 04 Mar 2009 23:52:47 +0100] rev 30267
removed old/broken CVS Ids;
wenzelm [Wed, 04 Mar 2009 23:05:32 +0100] rev 30266
ML antiquotation @{lemma}: allow 'and' list, proper simultaneous type-checking;
chaieb [Wed, 04 Mar 2009 19:22:32 +0000] rev 30265
merged
chaieb [Wed, 04 Mar 2009 19:21:56 +0000] rev 30264
Moved general theorems about sums and products to FiniteSet.thy
chaieb [Wed, 04 Mar 2009 19:21:56 +0000] rev 30263
fixed proofs; added rules as default simp-rules
chaieb [Wed, 04 Mar 2009 19:21:56 +0000] rev 30262
A formalization of Topology on Euclidean spaces, Includes limits (nets) , continuity, fixpoint theorems, homeomorphisms
chaieb [Wed, 04 Mar 2009 19:21:55 +0000] rev 30261
Added Libray dependency on Topology_Euclidean_Space
chaieb [Wed, 04 Mar 2009 19:21:55 +0000] rev 30260
Added general theorems for fold_image, setsum and set_prod
chaieb [Wed, 04 Mar 2009 19:21:28 +0000] rev 30259
fixed proofs
chaieb [Wed, 04 Mar 2009 10:54:47 +0000] rev 30258
merged
chaieb [Wed, 04 Mar 2009 10:33:14 +0000] rev 30257
merged
chaieb [Wed, 25 Feb 2009 10:29:01 +0000] rev 30256
merged
chaieb [Wed, 25 Feb 2009 10:28:49 +0000] rev 30255
merged
blanchet [Wed, 04 Mar 2009 18:18:05 +0100] rev 30254
Second try at adding "nitpick_const_def" attribute.
I don't know what happened the first time (change d8944fd4365e). It just vanished somehow.
blanchet [Wed, 04 Mar 2009 15:49:39 +0100] rev 30253
Fix parentheses.
blanchet [Wed, 04 Mar 2009 15:33:07 +0100] rev 30252
merged
blanchet [Wed, 04 Mar 2009 15:32:57 +0100] rev 30251
Added "nitpick_const_simp" attribute to Nominal primrec.
wenzelm [Wed, 04 Mar 2009 14:23:54 +0100] rev 30250
NEWS: renamed o2s to Option.set;
haftmann [Wed, 04 Mar 2009 13:42:23 +0100] rev 30249
less arbitrary occurrences of undefined
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
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);
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;
wenzelm [Tue, 03 Mar 2009 21:49:34 +0100] rev 30232
tuned str_of, now subject to verbose flag;
wenzelm [Tue, 03 Mar 2009 21:49:05 +0100] rev 30231
added @{binding} ML antiquotations;
wenzelm [Tue, 03 Mar 2009 21:48:40 +0100] rev 30230
added print_properties, print_position (again);
wenzelm [Tue, 03 Mar 2009 19:30:43 +0100] rev 30229
merged
haftmann [Tue, 03 Mar 2009 19:21:10 +0100] rev 30228
merged
haftmann [Tue, 03 Mar 2009 13:20:53 +0100] rev 30227
tuned manuals
haftmann [Tue, 03 Mar 2009 11:00:51 +0100] rev 30226
more canonical directory structure of manuals
wenzelm [Tue, 03 Mar 2009 18:33:21 +0100] rev 30225
merged
nipkow [Tue, 03 Mar 2009 17:05:18 +0100] rev 30224
removed and renamed redundant lemmas
wenzelm [Tue, 03 Mar 2009 18:32:01 +0100] rev 30223
renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
minor tuning;
wenzelm [Tue, 03 Mar 2009 18:31:59 +0100] rev 30222
moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
moved separator/is_qualified from binding.ML back to name_space.ML -- only name space introduces an explicit notation for qualified names;
type binding: maintain explicit qualifier, indepently of base name;
tuned signature of Binding: renamed name_pos to make, renamed base_name to name_of, renamed map_base to map_name, added mandatory flag to qualify, simplified map_prefix (formerly unused);
Binding.str_of: include markup with position properties;
misc tuning;
wenzelm [Tue, 03 Mar 2009 17:42:30 +0100] rev 30221
added markup for binding;
tuned;
wenzelm [Tue, 03 Mar 2009 15:12:52 +0100] rev 30220
Binding.str_of;
removed dead code;
tuned;
wenzelm [Tue, 03 Mar 2009 15:09:09 +0100] rev 30219
Binding.str_of;
pretty_name_atts: check Binding.is_empty, not result of Binding.str_of;
wenzelm [Tue, 03 Mar 2009 15:09:08 +0100] rev 30218
Binding.str_of;
wenzelm [Tue, 03 Mar 2009 15:09:07 +0100] rev 30217
renamed Binding.display to Binding.str_of, which is slightly more canonical;
tuned signature;
wenzelm [Tue, 03 Mar 2009 14:54:12 +0100] rev 30216
nicer_shortest: use NameSpace.extern_flags with disabled "features" instead of internal NameSpace.get_accesses;
wenzelm [Tue, 03 Mar 2009 14:53:29 +0100] rev 30215
moved name space externalization flags back to name_space.ML;
added pure version extern_flags;
do not export internal get_accesses;
wenzelm [Tue, 03 Mar 2009 14:52:13 +0100] rev 30214
moved name space externalization flags back to name_space.ML;
display: always show prefix for now;
tuned signature;
wenzelm [Tue, 03 Mar 2009 14:16:05 +0100] rev 30213
reverted change introduced in a7c164e228e1 -- there cannot be a "bug" in a perfectly normal operation on the internal data representation that merely escaped into public by accident (cf. 0a981c596372);
wenzelm [Tue, 03 Mar 2009 14:08:53 +0100] rev 30212
merged
wenzelm [Tue, 03 Mar 2009 14:07:43 +0100] rev 30211
Thm.binding;
wenzelm [Tue, 03 Mar 2009 14:07:23 +0100] rev 30210
added type binding and val empty_binding;
wenzelm [Tue, 03 Mar 2009 13:22:01 +0100] rev 30209
updated generated files;