wenzelm [Mon, 27 May 2013 21:00:30 +0200] rev 52187
tuned;
wenzelm [Mon, 27 May 2013 18:39:21 +0200] rev 52186
tuned;
wenzelm [Mon, 27 May 2013 18:24:38 +0200] rev 52185
discontinued obsolete show_all_types;
popescua [Mon, 27 May 2013 20:09:20 +0200] rev 52184
added Ordered_Union
popescua [Fri, 24 May 2013 19:09:56 +0200] rev 52183
fixed files broken due to Zorn changes (cf. 59e5dd7b8f9a)
popescua [Fri, 24 May 2013 18:11:57 +0200] rev 52182
well-order extension (by Christian Sternagel)
popescua [Fri, 24 May 2013 17:37:06 +0200] rev 52181
modernized Zorn (by Christian Sternagel)
wenzelm [Mon, 27 May 2013 16:53:21 +0200] rev 52180
merged
wenzelm [Mon, 27 May 2013 16:52:39 +0200] rev 52179
more thorough type unification: treat equal Vars like other atoms, otherwise unify type of term pair (not just accidental body_type of its head Vars);
wenzelm [Mon, 27 May 2013 15:57:38 +0200] rev 52178
instantiate types as well (see also Thm.first_order_match);
wenzelm [Mon, 27 May 2013 13:55:04 +0200] rev 52177
tuned;
wenzelm [Mon, 27 May 2013 13:44:02 +0200] rev 52176
updated to ProofGeneral-4.2;
wenzelm [Mon, 27 May 2013 12:40:50 +0200] rev 52175
uniform Term_Position.markers (cf. dbadb4d03cbc);
blanchet [Mon, 27 May 2013 15:14:41 +0200] rev 52174
get rid of "show_all_types" in Nitpick
blanchet [Mon, 27 May 2013 15:13:34 +0200] rev 52173
tuning
blanchet [Mon, 27 May 2013 15:00:01 +0200] rev 52172
killed dead argument
blanchet [Mon, 27 May 2013 14:00:32 +0200] rev 52171
tuning
blanchet [Mon, 27 May 2013 13:30:08 +0200] rev 52170
generalized "mk_co_iter" to handle mutualized (co)iterators
blanchet [Mon, 27 May 2013 12:21:17 +0200] rev 52169
tuning
nipkow [Mon, 27 May 2013 10:13:51 +0200] rev 52168
tuned
nipkow [Mon, 27 May 2013 09:15:26 +0200] rev 52167
tuned
nipkow [Mon, 27 May 2013 07:44:10 +0200] rev 52166
merged
nipkow [Mon, 27 May 2013 07:42:10 +0200] rev 52165
tuned
wenzelm [Sun, 26 May 2013 22:57:48 +0200] rev 52164
merged
wenzelm [Sun, 26 May 2013 22:47:00 +0200] rev 52163
position constraint for bound dummy -- more PIDE markup;
wenzelm [Sun, 26 May 2013 21:53:10 +0200] rev 52162
position constraint for dummy_pattern -- more PIDE markup;
wenzelm [Sun, 26 May 2013 21:05:03 +0200] rev 52161
tuned;
wenzelm [Sun, 26 May 2013 20:42:43 +0200] rev 52160
tuned signature;
wenzelm [Sun, 26 May 2013 20:08:53 +0200] rev 52159
tuned -- less ML compiler warnings;
wenzelm [Sun, 26 May 2013 20:03:47 +0200] rev 52158
more robust variant_free: avoid clash with consts name space (e.g. consts "x", "xa", etc.);
wenzelm [Sun, 26 May 2013 19:29:15 +0200] rev 52157
more uniform context;
wenzelm [Sun, 26 May 2013 19:27:32 +0200] rev 52156
tuned signature;
wenzelm [Sun, 26 May 2013 19:11:52 +0200] rev 52155
more conventional pretty printing;
more markup;
wenzelm [Sun, 26 May 2013 18:37:43 +0200] rev 52154
tuned white-space;
haftmann [Sun, 26 May 2013 19:45:54 +0200] rev 52153
more specific structure for registration into theory and dependency onto locale
haftmann [Sun, 26 May 2013 19:45:54 +0200] rev 52152
examples for interpretation into target
blanchet [Sun, 26 May 2013 14:02:03 +0200] rev 52151
disable SPASS's splitting if Isar proofs are desired, because these are not handled by the proof reconstruction code (and it's not clear how to handle them considering the lack of documentation)
blanchet [Sun, 26 May 2013 12:56:37 +0200] rev 52150
handle lambda-lifted problems in Isar construction code
nipkow [Sun, 26 May 2013 11:56:55 +0200] rev 52149
simpler proof through custom summation function
wenzelm [Sat, 25 May 2013 18:30:38 +0200] rev 52148
merged
wenzelm [Sat, 25 May 2013 17:40:44 +0200] rev 52147
tuned;
wenzelm [Sat, 25 May 2013 17:13:34 +0200] rev 52146
tuned;
wenzelm [Sat, 25 May 2013 17:08:43 +0200] rev 52145
tuned;
wenzelm [Sat, 25 May 2013 16:55:27 +0200] rev 52144
tuned;
wenzelm [Sat, 25 May 2013 15:37:53 +0200] rev 52143
syntax translations always depend on context;
wenzelm [Sat, 25 May 2013 15:00:53 +0200] rev 52142
updated keywords;
haftmann [Sat, 25 May 2013 15:44:29 +0200] rev 52141
weaker precendence of syntax for big intersection and union on sets
haftmann [Sat, 25 May 2013 15:44:08 +0200] rev 52140
tuned structure
noschinl [Sat, 25 May 2013 13:59:08 +0200] rev 52139
add lemma
haftmann [Fri, 24 May 2013 23:57:24 +0200] rev 52138
bookkeeping and input syntax for exact specification of names of symbols in generated code
haftmann [Fri, 24 May 2013 23:57:24 +0200] rev 52137
use generic data for code symbols for unified "code_printing" syntax for custom serialisations
haftmann [Fri, 24 May 2013 23:57:24 +0200] rev 52136
dedicated module for code symbol data
haftmann [Fri, 24 May 2013 23:57:24 +0200] rev 52135
symbol data covers class relations also
wenzelm [Fri, 24 May 2013 22:07:01 +0200] rev 52134
merged
wenzelm [Fri, 24 May 2013 17:14:06 +0200] rev 52133
proper internal error, not user error;
wenzelm [Fri, 24 May 2013 17:04:04 +0200] rev 52132
tuned;
wenzelm [Fri, 24 May 2013 17:00:46 +0200] rev 52131
tuned signature;
wenzelm [Fri, 24 May 2013 16:42:57 +0200] rev 52130
tuned;
wenzelm [Fri, 24 May 2013 15:32:02 +0200] rev 52129
unify types of bound variables in the same manner as Unify.new_dpair (which emphatically "Tries to unify types of the bound variables!");
wenzelm [Fri, 24 May 2013 15:13:25 +0200] rev 52128
tuned signature -- slightly more general operations (cf. term.ML);