huffman [Sat, 22 May 2010 12:56:33 -0700] rev 37081
simplify definition of eta_tac
huffman [Sat, 22 May 2010 12:36:50 -0700] rev 37080
remove fixrec_simp attribute; fixrec uses default simpset from theory context instead
huffman [Sat, 22 May 2010 10:02:07 -0700] rev 37079
remove cont2cont simproc; instead declare cont2cont rules as simp rules
huffman [Sat, 22 May 2010 08:30:40 -0700] rev 37078
domain package internal proofs use fixed set of continuity rules, rather than taking cont2cont rules from context
haftmann [Sat, 22 May 2010 11:01:59 +0200] rev 37077
merged
haftmann [Sat, 22 May 2010 10:13:02 +0200] rev 37076
modernized sorting algorithms; quicksort implements sort
haftmann [Sat, 22 May 2010 10:12:50 +0200] rev 37075
modernized sorting algorithms; quicksort implements sort
haftmann [Sat, 22 May 2010 10:12:49 +0200] rev 37074
localized properties_for_sort
wenzelm [Mon, 24 May 2010 23:19:40 +0200] rev 37073
@tailrec annotation;
wenzelm [Mon, 24 May 2010 23:01:51 +0200] rev 37072
renamed "rev" to "reverse" following usual Scala conventions;
wenzelm [Sat, 22 May 2010 23:59:09 +0200] rev 37071
parse_spans: cover full range including adjacent well-formed commands -- intermediate ignored and malformed commands are reparsed as well;
wenzelm [Sat, 22 May 2010 23:53:09 +0200] rev 37070
added rev_iterator;
wenzelm [Sat, 22 May 2010 22:30:43 +0200] rev 37069
tuned;
wenzelm [Sat, 22 May 2010 22:30:37 +0200] rev 37068
access statically typed dockable windows;
wenzelm [Sat, 22 May 2010 22:05:41 +0200] rev 37067
simplified dockables using class Dockable;
wenzelm [Sat, 22 May 2010 21:48:01 +0200] rev 37066
generic dockable window;
wenzelm [Sat, 22 May 2010 20:59:55 +0200] rev 37065
separate event bus and dockable for raw output (stdout);
wenzelm [Sat, 22 May 2010 20:37:59 +0200] rev 37064
more Mac OS problems;
wenzelm [Sat, 22 May 2010 20:37:20 +0200] rev 37063
ignore system messages;
wenzelm [Sat, 22 May 2010 20:20:51 +0200] rev 37062
use proper ISABELLE_PLATFORM instead of adhoc uname;
wenzelm [Sat, 22 May 2010 20:10:11 +0200] rev 37061
refrain from using bold within the term language -- looks odd in Lobo with error/warning background;
wenzelm [Sat, 22 May 2010 20:02:26 +0200] rev 37060
tuned;
wenzelm [Sat, 22 May 2010 20:00:28 +0200] rev 37059
removed timing;
wenzelm [Sat, 22 May 2010 19:42:20 +0200] rev 37058
rendering information and style sheets via settings;
generalized Isabelle_System.try_read;
prefer getenv_strict in most situations;
wenzelm [Fri, 21 May 2010 23:48:48 +0200] rev 37057
more brackets -- unaligned to prevent odd auto-indentation;
wenzelm [Fri, 21 May 2010 23:21:40 +0200] rev 37056
merged
haftmann [Fri, 21 May 2010 17:16:16 +0200] rev 37055
adjusted to changes in Mapping.thy
haftmann [Fri, 21 May 2010 15:28:25 +0200] rev 37054
merged
haftmann [Fri, 21 May 2010 15:22:37 +0200] rev 37053
tuned
haftmann [Fri, 21 May 2010 15:22:37 +0200] rev 37052
more lemmas about mappings, in particular keys
haftmann [Fri, 21 May 2010 15:22:36 +0200] rev 37051
refined
haftmann [Fri, 21 May 2010 11:50:34 +0200] rev 37050
nats in Haskell are readable
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 21 May 2010 10:40:59 +0200] rev 37049
Let rsp and prs in fun_rel/fun_map format
wenzelm [Fri, 21 May 2010 23:19:27 +0200] rev 37048
tuned zoom_box;
tuned tooltips;
wenzelm [Fri, 21 May 2010 22:08:13 +0200] rev 37047
print calculation result in the context where the fact is actually defined -- proper externing;
misc tuning;
wenzelm [Fri, 21 May 2010 21:28:31 +0200] rev 37046
future_job: propagate current Position.thread_data to the forked job -- this is important to provide a default position, e.g. for parallelizied Goal.prove within a package (proper command transactions are wrapped via Toplevel.setmp_thread_position);
wenzelm [Fri, 21 May 2010 20:46:00 +0200] rev 37045
some message styling;
wenzelm [Fri, 21 May 2010 20:10:45 +0200] rev 37044
simplified message markup, using plain XML.Elem directly;
wenzelm [Fri, 21 May 2010 18:10:19 +0200] rev 37043
more robust Position.setmp_thread_data, independently of Output.debugging (essentially reverts f9ec18f7c0f6, which was motivated by clean exception_trace, but without transaction positions the Isabelle_Process protocol breaks down);
wenzelm [Fri, 21 May 2010 17:26:42 +0200] rev 37042
refrain from forcing a hardwired SHELL value, cf. 1494ded298a6 but it becomes obsolete again in 549969a7f582 and follow-ups;
wenzelm [Fri, 21 May 2010 16:49:33 +0200] rev 37041
bad_result: report fully explicit message;
wenzelm [Fri, 21 May 2010 16:40:25 +0200] rev 37040
observe additional isabelle-jedit.css for component and user;
visial separation of message divs;
wenzelm [Fri, 21 May 2010 15:29:20 +0200] rev 37039
added checkboxes for debug/tracing filter;
misc tuning;
wenzelm [Fri, 21 May 2010 14:53:19 +0200] rev 37038
more abstract view on prover output messages;
wenzelm [Fri, 21 May 2010 12:59:44 +0200] rev 37037
added some tooltips;
wenzelm [Fri, 21 May 2010 11:51:03 +0200] rev 37036
HTML_Panel.handler as overridable method;
wenzelm [Fri, 21 May 2010 11:50:19 +0200] rev 37035
added Library.undefined (in Scala);
wenzelm [Fri, 21 May 2010 11:16:01 +0200] rev 37034
more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
do not re-use mutable DOM -- avoid races wrt. the rendering engine;
more thorough resize -- always recalculate metrics/margin synchronously;
asynchronous setDocument;
tuned;
wenzelm [Fri, 21 May 2010 11:12:54 +0200] rev 37033
component resize: full handle_resize;
huffman [Thu, 20 May 2010 21:19:38 -0700] rev 37032
speed up some proofs and fix some warnings
wenzelm [Thu, 20 May 2010 23:22:37 +0200] rev 37031
merged
haftmann [Thu, 20 May 2010 19:55:42 +0200] rev 37030
merged
haftmann [Thu, 20 May 2010 18:00:48 +0200] rev 37029
proper code generator for complement
haftmann [Thu, 20 May 2010 17:35:02 +0200] rev 37028
proper document text
haftmann [Thu, 20 May 2010 17:29:43 +0200] rev 37027
implement Mapping.map_entry
haftmann [Thu, 20 May 2010 17:29:43 +0200] rev 37026
operations default, map_entry, map_default; more lemmas