blanchet [Mon, 26 Aug 2013 12:14:41 +0200] rev 53202
export one more ML function, needed for primcorec
blanchet [Mon, 26 Aug 2013 12:14:40 +0200] rev 53201
reverted 6c5e7143e1f6; took a better look at evaluation data this time
wenzelm [Mon, 26 Aug 2013 11:42:35 +0200] rev 53200
tuned unchecked ML;
wenzelm [Mon, 26 Aug 2013 11:41:17 +0200] rev 53199
removed junk;
wenzelm [Mon, 26 Aug 2013 10:33:16 +0200] rev 53198
ignore trailing primes, e.g. rename \<alpha>' to \<alpha>'' instead of \<alpha>'a;
blanchet [Mon, 26 Aug 2013 09:07:32 +0200] rev 53197
tuned fudge factor in light of evaluation
wenzelm [Sun, 25 Aug 2013 23:20:25 +0200] rev 53196
tuned proofs;
wenzelm [Sun, 25 Aug 2013 21:25:17 +0200] rev 53195
tuned proofs;
wenzelm [Sun, 25 Aug 2013 20:57:09 +0200] rev 53194
discontinued rendering of obsolete \<onesuperior>, \<twosuperior>, \<threesuperior>;
wenzelm [Sun, 25 Aug 2013 20:43:10 +0200] rev 53193
tuned;
wenzelm [Sun, 25 Aug 2013 20:32:26 +0200] rev 53192
maintain goal forks as part of global execution;
tuned;
wenzelm [Sun, 25 Aug 2013 17:17:48 +0200] rev 53191
tuned proofs -- fewer warnings;
wenzelm [Sun, 25 Aug 2013 17:04:22 +0200] rev 53190
simplified Goal.forked_proofs: status is determined via group instead of dummy future (see also Pure/PIDE/execution.ML);
clarified Task_Queue.group_status;
tuned;
wenzelm [Sun, 25 Aug 2013 16:03:12 +0200] rev 53189
discontinued parallel_subproofs_saturation and related internal counters (superseded by parallel_subproofs_threshold and timing information);
simplified Goal.future_enabled;
wenzelm [Sun, 25 Aug 2013 14:35:25 +0200] rev 53188
some secondary shortcuts derived from 5.1.0/keymaps/German_Keyboard_keys.props (using CIRCUMFLEX instead of S+1);
tuned;
wenzelm [Sun, 25 Aug 2013 13:59:40 +0200] rev 53187
use view root as parent for popup, which provides more space and avoids confusion of mouse wheel handlers on Windows (wrt. text area scrollbar);
wenzelm [Sat, 24 Aug 2013 23:16:37 +0200] rev 53186
tuned proofs;
wenzelm [Sat, 24 Aug 2013 21:23:40 +0200] rev 53185
tuned proofs;
wenzelm [Sat, 24 Aug 2013 18:29:23 +0200] rev 53184
confine popup to parent component, to avoid javax.swing.PopupFactory$HeavyWeightPopup and its problems with Linux window management and Mac OS X key handling;
wenzelm [Sat, 24 Aug 2013 17:41:57 +0200] rev 53183
strict checking of coordinates wrt. inner painter component;
wenzelm [Sat, 24 Aug 2013 17:39:18 +0200] rev 53182
more static values;
wenzelm [Sat, 24 Aug 2013 16:06:15 +0200] rev 53181
support more brackets;
wenzelm [Sat, 24 Aug 2013 15:34:09 +0200] rev 53180
prefer static "control", which is determined when the mouse event happens, not when its action runs;
wenzelm [Sat, 24 Aug 2013 15:30:50 +0200] rev 53179
tuned signature;
wenzelm [Sat, 24 Aug 2013 14:58:36 +0200] rev 53178
more precise painting;
wenzelm [Sat, 24 Aug 2013 13:32:51 +0200] rev 53177
more uniform treatment of Swing_Thread context switch: prefer asynchronous Swing_Thread.later from actor;
wenzelm [Sat, 24 Aug 2013 12:31:24 +0200] rev 53176
clarified border (again, see also 7ce3ebc268a1);
wenzelm [Sat, 24 Aug 2013 00:06:53 +0200] rev 53175
more faithful representation of U+2983 and U+2984 as "white" curly braces -- based on braces and bar from cmsy10.pfb;
wenzelm [Fri, 23 Aug 2013 22:48:12 +0200] rev 53174
prefer plain subscript for notation;
wenzelm [Fri, 23 Aug 2013 21:59:29 +0200] rev 53173
merged
wenzelm [Fri, 23 Aug 2013 20:53:00 +0200] rev 53172
more standard parser combinator expressions and tool setup;
wenzelm [Fri, 23 Aug 2013 20:35:50 +0200] rev 53171
added Theory.setup convenience;
wenzelm [Fri, 23 Aug 2013 20:09:34 +0200] rev 53170
more robust ML_Antiquote.variant via Name.desymbolize (which also allows symbolic names, for example);
wenzelm [Fri, 23 Aug 2013 19:53:27 +0200] rev 53169
clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
subtle change of semantics of ML_Context.add_antiq: need to avoid accidental update of context due to concrete syntax parser (cf. Scan.pass);
wenzelm [Fri, 23 Aug 2013 17:01:12 +0200] rev 53168
tuned signature;
wenzelm [Fri, 23 Aug 2013 15:36:54 +0200] rev 53167
discontinued unused antiquotation blocks;
wenzelm [Fri, 23 Aug 2013 15:04:00 +0200] rev 53166
missing ROOT (cf. beb4ee344c22);
wenzelm [Fri, 23 Aug 2013 12:43:16 +0200] rev 53165
more modular setup;
wenzelm [Fri, 23 Aug 2013 12:40:55 +0200] rev 53164
clarified position of Spec_Check for Isabelle/ML -- it is unrelated to Isabelle/HOL;
just one src/Tools/ROOT;
wenzelm [Fri, 23 Aug 2013 12:30:51 +0200] rev 53163
removed unused ML antiquotations @{let}, @{note};
wenzelm [Fri, 23 Aug 2013 11:44:28 +0200] rev 53162
obsolete (see 52790e3961fe);
wenzelm [Fri, 23 Aug 2013 11:41:17 +0200] rev 53161
added action isabelle.reset-font-size;
wenzelm [Fri, 23 Aug 2013 11:23:26 +0200] rev 53160
tuned -- some reformatting;
blanchet [Fri, 23 Aug 2013 16:51:53 +0200] rev 53159
repaired num_extra_feature_facts + tuning
blanchet [Fri, 23 Aug 2013 16:14:26 +0200] rev 53158
thread information about when a constant became relevant through MePo -- the information is not used yet but could help fight starvation in the (ITP) world
blanchet [Fri, 23 Aug 2013 16:02:32 +0200] rev 53157
removed obsolete file
blanchet [Fri, 23 Aug 2013 15:49:27 +0200] rev 53156
minor MaSh fix
blanchet [Fri, 23 Aug 2013 15:07:32 +0200] rev 53155
eliminated some needless MaSh features
blanchet [Fri, 23 Aug 2013 14:19:57 +0200] rev 53154
tuned output
blanchet [Fri, 23 Aug 2013 14:04:08 +0200] rev 53153
better tracing + honor blocking better
blanchet [Fri, 23 Aug 2013 13:30:25 +0200] rev 53152
learn new facts on query if there aren't too many of them in MaSh
kuncar [Fri, 23 Aug 2013 00:12:20 +0200] rev 53151
remove OP
blanchet [Thu, 22 Aug 2013 23:03:23 +0200] rev 53150
increase relevance of unknown proximate facts
blanchet [Thu, 22 Aug 2013 23:03:22 +0200] rev 53149
fixed pattern matching
blanchet [Thu, 22 Aug 2013 23:03:21 +0200] rev 53148
fixed subtle bug with "take" + thread overlord through
haftmann [Thu, 22 Aug 2013 21:15:43 +0200] rev 53147
separate tracing option for code_simp
haftmann [Thu, 22 Aug 2013 21:15:43 +0200] rev 53146
congruence rules for code_simp to mimic typical non-strict behaviour of conj and disj
kuncar [Thu, 22 Aug 2013 17:19:51 +0200] rev 53145
delete corresponding compound lhs and rhs when a transfer rule is deleted; tuned
kuncar [Thu, 22 Aug 2013 17:19:44 +0200] rev 53144
publish a private function
traytel [Thu, 22 Aug 2013 17:13:46 +0200] rev 53143
configuration option to control timing output for (co)datatypes