wenzelm [Tue, 16 Feb 2010 13:26:21 +0100] rev 35143
comment;
wenzelm [Tue, 16 Feb 2010 13:06:43 +0100] rev 35142
conceal internal record definitions;
wenzelm [Tue, 16 Feb 2010 11:59:05 +0100] rev 35141
simplified meaning of ProofContext.verbose;
eliminated strange ProofContext.setmp_verbose_CRITICAL;
less confusing printing of (cumulative) unnamed facts;
wenzelm [Tue, 16 Feb 2010 11:56:13 +0100] rev 35140
refrain from using @{const_name} in syntax translations;
wenzelm [Tue, 16 Feb 2010 11:27:29 +0100] rev 35139
misc tuning and simplification;
wenzelm [Mon, 15 Feb 2010 23:58:24 +0100] rev 35138
refined and exported record_info;
wenzelm [Mon, 15 Feb 2010 22:40:03 +0100] rev 35137
modernized structures;
wenzelm [Mon, 15 Feb 2010 22:24:19 +0100] rev 35136
modernized signature -- proper binding;
misc tuning;
wenzelm [Mon, 15 Feb 2010 20:32:21 +0100] rev 35135
tuned errors;
tuned;
wenzelm [Mon, 15 Feb 2010 20:30:56 +0100] rev 35134
Typedef.the_info;
wenzelm [Mon, 15 Feb 2010 20:01:07 +0100] rev 35133
formal markup of constants;
misc tuning;
wenzelm [Mon, 15 Feb 2010 19:16:45 +0100] rev 35132
tuned document;
wenzelm [Mon, 15 Feb 2010 18:50:16 +0100] rev 35131
eliminated old fold;
wenzelm [Mon, 15 Feb 2010 18:03:42 +0100] rev 35130
renamed InfixName to Infix etc.;
wenzelm [Mon, 15 Feb 2010 17:17:51 +0100] rev 35129
discontinued unnamed infix syntax;
wenzelm [Mon, 15 Feb 2010 15:50:41 +0100] rev 35128
eliminated unnamed infixes;
haftmann [Mon, 15 Feb 2010 14:04:06 +0100] rev 35127
apply global morphism for theory, instantiation and overloading target; n.b. target morphism and global morphism coincide for theory target
haftmann [Mon, 15 Feb 2010 14:04:06 +0100] rev 35126
clarifed type
boehmes [Sun, 14 Feb 2010 17:46:28 +0100] rev 35125
optionally localize assertion labels (based on user-defined offsets) to reduce the effort of label adaptions after changes to the source program
wenzelm [Sun, 14 Feb 2010 00:26:48 +0100] rev 35124
formal markup of constants;
wenzelm [Sat, 13 Feb 2010 23:24:57 +0100] rev 35123
modernized structures;
wenzelm [Sat, 13 Feb 2010 23:16:06 +0100] rev 35122
authentic proof syntax;
haftmann [Fri, 12 Feb 2010 14:28:01 +0100] rev 35121
tuned import order
haftmann [Fri, 12 Feb 2010 09:49:28 +0100] rev 35120
tuned comments
wenzelm [Thu, 11 Feb 2010 23:50:38 +0100] rev 35119
merged
huffman [Thu, 11 Feb 2010 12:26:50 -0800] rev 35118
merged
huffman [Thu, 11 Feb 2010 12:26:07 -0800] rev 35117
change generated lemmas dist_eqs and dist_les to iff-style
boehmes [Thu, 11 Feb 2010 17:48:55 +0100] rev 35116
unfold quantifiers (Ball, Bex, Ex1)