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