| Sun, 23 May 2010 10:37:43 +0100 |
webertj |
Refactoring, minor extensions (e.g., church_rosser).
|
changeset |
files
|
| Sat, 22 May 2010 17:44:12 -0700 |
huffman |
NEWS: removed fixrec_simp attribute
|
changeset |
files
|
| Sat, 22 May 2010 16:46:18 -0700 |
huffman |
merged
|
changeset |
files
|
| Sat, 22 May 2010 16:45:46 -0700 |
huffman |
disambiguate some syntax
|
changeset |
files
|
| Sat, 22 May 2010 14:04:05 -0700 |
huffman |
optimize continuity proofs in fixrec package, using cont2cont rules
|
changeset |
files
|
| Sat, 22 May 2010 13:40:15 -0700 |
huffman |
add beta_cfun simproc, which uses cont2cont rules
|
changeset |
files
|
| Sat, 22 May 2010 13:27:36 -0700 |
huffman |
removed fixrec_simp attribute (cf. a2a1c8a658ef)
|
changeset |
files
|
| Sat, 22 May 2010 12:56:33 -0700 |
huffman |
simplify definition of eta_tac
|
changeset |
files
|
| Sat, 22 May 2010 12:36:50 -0700 |
huffman |
remove fixrec_simp attribute; fixrec uses default simpset from theory context instead
|
changeset |
files
|
| Sat, 22 May 2010 10:02:07 -0700 |
huffman |
remove cont2cont simproc; instead declare cont2cont rules as simp rules
|
changeset |
files
|
| Sat, 22 May 2010 08:30:40 -0700 |
huffman |
domain package internal proofs use fixed set of continuity rules, rather than taking cont2cont rules from context
|
changeset |
files
|
| Sat, 22 May 2010 11:01:59 +0200 |
haftmann |
merged
|
changeset |
files
|
| Sat, 22 May 2010 10:13:02 +0200 |
haftmann |
modernized sorting algorithms; quicksort implements sort
|
changeset |
files
|
| Sat, 22 May 2010 10:12:50 +0200 |
haftmann |
modernized sorting algorithms; quicksort implements sort
|
changeset |
files
|
| Sat, 22 May 2010 10:12:49 +0200 |
haftmann |
localized properties_for_sort
|
changeset |
files
|
| Mon, 24 May 2010 23:19:40 +0200 |
wenzelm |
@tailrec annotation;
|
changeset |
files
|
| Mon, 24 May 2010 23:01:51 +0200 |
wenzelm |
renamed "rev" to "reverse" following usual Scala conventions;
|
changeset |
files
|
| Sat, 22 May 2010 23:59:09 +0200 |
wenzelm |
parse_spans: cover full range including adjacent well-formed commands -- intermediate ignored and malformed commands are reparsed as well;
|
changeset |
files
|
| Sat, 22 May 2010 23:53:09 +0200 |
wenzelm |
added rev_iterator;
|
changeset |
files
|
| Sat, 22 May 2010 22:30:43 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 22 May 2010 22:30:37 +0200 |
wenzelm |
access statically typed dockable windows;
|
changeset |
files
|
| Sat, 22 May 2010 22:05:41 +0200 |
wenzelm |
simplified dockables using class Dockable;
|
changeset |
files
|
| Sat, 22 May 2010 21:48:01 +0200 |
wenzelm |
generic dockable window;
|
changeset |
files
|
| Sat, 22 May 2010 20:59:55 +0200 |
wenzelm |
separate event bus and dockable for raw output (stdout);
|
changeset |
files
|
| Sat, 22 May 2010 20:37:59 +0200 |
wenzelm |
more Mac OS problems;
|
changeset |
files
|
| Sat, 22 May 2010 20:37:20 +0200 |
wenzelm |
ignore system messages;
|
changeset |
files
|
| Sat, 22 May 2010 20:20:51 +0200 |
wenzelm |
use proper ISABELLE_PLATFORM instead of adhoc uname;
|
changeset |
files
|
| Sat, 22 May 2010 20:10:11 +0200 |
wenzelm |
refrain from using bold within the term language -- looks odd in Lobo with error/warning background;
|
changeset |
files
|
| Sat, 22 May 2010 20:02:26 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 22 May 2010 20:00:28 +0200 |
wenzelm |
removed timing;
|
changeset |
files
|
| Sat, 22 May 2010 19:42:20 +0200 |
wenzelm |
rendering information and style sheets via settings;
|
changeset |
files
|
| Fri, 21 May 2010 23:48:48 +0200 |
wenzelm |
more brackets -- unaligned to prevent odd auto-indentation;
|
changeset |
files
|
| Fri, 21 May 2010 23:21:40 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 21 May 2010 17:16:16 +0200 |
haftmann |
adjusted to changes in Mapping.thy
|
changeset |
files
|
| Fri, 21 May 2010 15:28:25 +0200 |
haftmann |
merged
|
changeset |
files
|
| Fri, 21 May 2010 15:22:37 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Fri, 21 May 2010 15:22:37 +0200 |
haftmann |
more lemmas about mappings, in particular keys
|
changeset |
files
|
| Fri, 21 May 2010 15:22:36 +0200 |
haftmann |
refined
|
changeset |
files
|
| Fri, 21 May 2010 11:50:34 +0200 |
haftmann |
nats in Haskell are readable
|
changeset |
files
|
| Fri, 21 May 2010 10:40:59 +0200 |
Cezary Kaliszyk |
Let rsp and prs in fun_rel/fun_map format
|
changeset |
files
|
| Fri, 21 May 2010 23:19:27 +0200 |
wenzelm |
tuned zoom_box;
|
changeset |
files
|
| Fri, 21 May 2010 22:08:13 +0200 |
wenzelm |
print calculation result in the context where the fact is actually defined -- proper externing;
|
changeset |
files
|
| Fri, 21 May 2010 21:28:31 +0200 |
wenzelm |
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);
|
changeset |
files
|
| Fri, 21 May 2010 20:46:00 +0200 |
wenzelm |
some message styling;
|
changeset |
files
|
| Fri, 21 May 2010 20:10:45 +0200 |
wenzelm |
simplified message markup, using plain XML.Elem directly;
|
changeset |
files
|
| Fri, 21 May 2010 18:10:19 +0200 |
wenzelm |
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);
|
changeset |
files
|
| Fri, 21 May 2010 17:26:42 +0200 |
wenzelm |
refrain from forcing a hardwired SHELL value, cf. 1494ded298a6 but it becomes obsolete again in 549969a7f582 and follow-ups;
|
changeset |
files
|
| Fri, 21 May 2010 16:49:33 +0200 |
wenzelm |
bad_result: report fully explicit message;
|
changeset |
files
|
| Fri, 21 May 2010 16:40:25 +0200 |
wenzelm |
observe additional isabelle-jedit.css for component and user;
|
changeset |
files
|
| Fri, 21 May 2010 15:29:20 +0200 |
wenzelm |
added checkboxes for debug/tracing filter;
|
changeset |
files
|
| Fri, 21 May 2010 14:53:19 +0200 |
wenzelm |
more abstract view on prover output messages;
|
changeset |
files
|
| Fri, 21 May 2010 12:59:44 +0200 |
wenzelm |
added some tooltips;
|
changeset |
files
|
| Fri, 21 May 2010 11:51:03 +0200 |
wenzelm |
HTML_Panel.handler as overridable method;
|
changeset |
files
|
| Fri, 21 May 2010 11:50:19 +0200 |
wenzelm |
added Library.undefined (in Scala);
|
changeset |
files
|
| Fri, 21 May 2010 11:16:01 +0200 |
wenzelm |
more systematic treatment of internal state, which belongs strictly to the main actor, not the Swing thread;
|
changeset |
files
|
| Fri, 21 May 2010 11:12:54 +0200 |
wenzelm |
component resize: full handle_resize;
|
changeset |
files
|
| Thu, 20 May 2010 21:19:38 -0700 |
huffman |
speed up some proofs and fix some warnings
|
changeset |
files
|
| Thu, 20 May 2010 23:22:37 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Thu, 20 May 2010 19:55:42 +0200 |
haftmann |
merged
|
changeset |
files
|
| Thu, 20 May 2010 18:00:48 +0200 |
haftmann |
proper code generator for complement
|
changeset |
files
|